Skip to content

Latest commit

 

History

History
81 lines (50 loc) · 1.5 KB

README.md

File metadata and controls

81 lines (50 loc) · 1.5 KB
Raw

logicamente

A first-order logic theorem prover.

Dependencies

  • Python 3.7 (for @dataclass decorator)
  • pyparsing 2.3.1

Available on pip, install with pip install pyparsing

Running

Just

python3 main.py

The program asks for a Prolog-like knowledge base file and for a query.

There's an included example file called underground

Example usage:

$ python main.py

input file: ./underground

input query: reachable(tottenham_court_road,leicester_square, R)

backward_chain{ (reachable(tottenham_court_road, leicester_square, R)) }: True

result: (reachable(tottenham_court_road, leicester_square, (list())))

Knowledge base quick start

  • Variables: upper case + _

  • Literals: lower case + _

  • N-ary relations are supported, name same as literals

  • (A & B) => C (implication) becomes C :- A, B

  • Body of clause

  • Lists: brackets, comma-separated [a, B, foo(bar, Q)]

  • Every clause must end with .

  • Clauses are resolved using the order provided in the KB file. If there is a cycle it will be detected and can be corrected by changing the clauses' order.

  • C-style comments supported

Example:

/* file: happy.pl */
smiles(P, Q) :- happy(P).
happy(P) :- loves(P, Q), rested(P).

rested(johnny).
loves(mary, johnny).

loves(P,Q) :- loves(Q,P).

$ python main.py
input file: happy.pl
input query: happy(X)
backward_chain{ (happy(X)) }: True
result: (happy(johnny))

Thanks to: https://stackoverflow.com/a/28398903 for Python implementation of Visitor pattern! :)