eyekind is a Python rule language with forward and backward reasoning and checkable proofs. You write facts and rules in plain Python; eyekind draws conclusions, and every conclusion can come with a proof that a separate checker verifies against your program. It runs as a command-line program, a Python library, and a browser application, with no dependencies.
- Playground: run programs in your browser.
- Guide: run programs, write rules, check proofs, use the library, and develop eyekind.
- Specification: the language, its canonical text, the proof format, and the C1–C8 checks.
- Examples: 94 runnable programs, each with a card deck and saved conclusions, proofs and check reports.
- Conformance suite: 400 cases that test any implementation of the specification through its command line.
fact(type('socrates', 'human'))
fact(subclass_of('human', 'mortal'))
implies([type(S, A), subclass_of(A, B)], type(S, B))
query(type(X, Y))
Install it with pip install eyekind for the eyekind command, or run it
from a checkout with bin/eyekind.py or python -m eyekind:
python -m eyekind examples/socrates.py
python -m eyekind -c examples/socrates.py
python -m eyekind --proof examples/socrates.py > /tmp/proof.py
python -m eyekind --check-proof /tmp/proof.py examples/socrates.py
MIT licensed; see LICENSE.md.