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.
Publications
- 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.
People
- Aboubakr Achraf El Ghazi
- Mana Taghdiri
- Mihai Herda
Tool
We will be happy to share the tool upon your request. Please feel free to send an email to A. Achraf El Ghazi or Mana Taghdiri.