Discover rispoli/acl-lean Open Source project

Stars
1
Language
Prolog
License
GNU Affero Genera...
Created almost 12 years ago
Updated almost 12 years ago

rispoli

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

A theorem prover for propositional access control logic with "says" operator. Implements Seq-ACL, an analytic labeled sequent calculus for access control logic along with an automatic generation of human-readable proofs. Main implementation in SWI-Prolog with translation to GNU-Prolog and relative C bindings provided.

secommunity

A collection of tools that can be used to define distributed access control policies using an extension of the Answer Set Programming system DLV. In particular, several external predicates were developed, which can be used via DLV-Complex, with the aim to query remote knowledge bases. A server that handles such queries using its own local DLV-Complex instance was also written in the context of this work.

C++

nesy

Neural-Symbolic Rule-Based Monitoring.

Prolog

delegation2spass

A reducer and translator for a set of complete reduction axioms. Simplifies dynamic formulae for a delegation/revocation logic and converts them into propositional logic expressed in DFG syntax.

Scheme

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.

Prolog