Formal Logic Framework
Project description
#forseti [](https://travis-ci.org/MasterOdin/forseti) [](https://coveralls.io/r/MasterOdin/forseti?branch=master) [](https://landscape.io/github/MasterOdin/forseti/master) [](https://pypi.python.org/pypi/forseti/) [](https://pypi.python.org/pypi/forseti/) [](https://pypi.python.org/pypi/forseti/) [](https://pypi.python.org/pypi/forseti/)
A Formal Logic framework for a variety of applications.
##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: `python 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 `python 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. Formal Logic Prover 1. Optimizations
##Goals: Using forseti to implement the following programs/applications
1. Automated Theorem Prover (done in forseti core) 1. [Implement Davis-Putnam Algorithm](http://en.wikipedia.org/wiki/Davis%E2%80%93Putnam_algorithm) 1. [Truth Trees](http://legacy.earlham.edu/~peters/courses/log/treeprop.htm) 1. [Slate](http://rair.cogsci.rpi.edu/projects/slate/)/[Fitch](http://en.wikipedia.org/wiki/Fitch-style_calculus)