forseti

Formal Logic Framework


License
MIT
Install
pip install forseti==0.8.1

Documentation

forseti

Build Status Coverage Status Code Health

A Formal Logic framework for a variety of applications.

Installation

From PyPI

forseti is available on PyPI.

$ pip install forseti

From source

  • Download the source code:
$ git clone git@github.com:MasterOdin/forseti.git
$ python setup.py install

Usage

forseti comes with an internal representation of propositional calculus formulas (atomic, not, and, or, implication, and equivalance). It can generate this from a functional representation of any formula. Interally, it holds everything as formula objects, which can take in other formulas as appropriate (Symbols can only hold one string).

An example:

from forseti import parser
from forseti.predicate import Atomic, And
assert parser.parse("and(a, b)") == And(Atomic('a'), Atomic('b'))

Additionally, it also comes with a builtin prover that can validate a propositional calculus argument

from forseti.prover import Prover
prover = Prover()
prover.add_formula("if(A,and(B,C))")
prover.add_formula("iff(C,B)")
prover.add_formula("not(C)")
prover.add_goal("not(A)")
assert_true(prover.run_prover())

Roadmap

  1. First Order Logic Prover
  2. Optimizations

Usages

These projects use forseti at their core:

  1. Truth Tables

Goals

Using forseti to implement the following programs/applications

  1. Automated Theorem Prover (done in forseti core)
  2. Implement Davis-Putnam Algorithm
  3. Truth Trees
  4. Slate / Fitch