GitHub - rispoli/seq-acl: A decidable theorem prover for the modal access control logic "ACL+". Implements an analytic labeled sequent calculus for access control logic along with an automatic generation of human-readable proofs.

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 9 Commits
examples		examples
README		README
deduction_tree.pl		deduction_tree.pl
depth_distance.pl		depth_distance.pl
inference_rules_axioms.pl		inference_rules_axioms.pl
latexify.pl		latexify.pl
m2dot.pl		m2dot.pl
makefile		makefile
op_pri.pl		op_pri.pl

Repository files navigation

Seq-ACL+: A Decidable Theorem Prover for ACL+

To lunch Seq-ACL+

1. Run SWI-Prolog ($ swipl)
2. Load latexify package (?- [latexify].)

Now you can prove formulas by typing

?- prove(a->a).

Or you can run test files as follows

?- ['examples/tests.pl'].

About

A decidable theorem prover for the modal access control logic "ACL+". Implements an analytic labeled sequent calculus for access control logic along with an automatic generation of human-readable proofs.

Readme