TCProver: A Prover for the FOL+TC Fragment
TCProver is a full automatic tool for proving valid formulas of the fragment of first-order logic enriched with (finite) relations and transitive closure (TC). TCProver focuses in its current version on Alloy -- a declarative first-order relational logic with built-in operators for transitive closure and cardinality.
TCProver uses an approach based on a basic non complete first-order axiomatization of TC together with an algorithm for detecting and injecting so-called R-Path invariants. Given a formula F that includes the transitive closure of a relation R, our approach can deduce a complete (pure) first-order axiomatization of the paths of R that occur in F . Such axiomatization enables full automated verification of F using an automatic theorem prover like Z3.
- First-Order Transitive Closure Axiomatization via Iterative Invariant Injections, Aboubakr Achraf El Ghazi, Mana Taghdiri, Mihai Herda. In NASA Formal Methods Symposium (NFM), 2015.
- Relational Reasoning via SMT Solving, Aboubakr Achraf El Ghazi, Mana Taghdiri. In International Symposium on Formal Methods (FM), 2011.