Skip to content

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.

Notifications You must be signed in to change notification settings

rispoli/seq-acl

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.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published