Injective transition graphs simplify checking cyclic proof termination
Global Trace Condition for Injective Transition Graphs
Logic in Computer Science
Summary
Ensuring that certain logical proofs stop and don’t loop forever is important in computer science. The authors describe a new way to represent these proofs using special graphs called injective transition graphs. They show that checking a simpler condition on these graphs is enough to guarantee the proofs will terminate, which can make verification easier. This connects ideas from proof theory and program termination analysis.
What this means in practice
- •For verification engineers: Use simplified graph conditions to verify termination in cyclic proofs for automated theorem proving systems.
- •For program analyzers: Improve termination analysis tools by applying weaker conditions on injective graphs to detect guaranteed program halting.
A theory result. No direct application yet.
Authors
Stefano Berardi, Ugo de'Liguoro, Daniel Osorio-Valencia
Abstract
We formulate the global trace condition, GTC, for cyclic proofs as a particular case of the size-change termination condition, or SCT. We express cyclic proofs through a variant of size-change graphs, called transition graphs, whose edges are labelled by (finite) bipartite relations. We show that injective transition graphs suffice to encode cyclic pre-proofs for a variant of Brotherston and Simpson's sequent calculus with inductive definitions. The injectivity of transition graphs corresponds to restricting SCT to fan-in-free graphs. Then we prove that an essentially weaker condition implies SCT in this case, and hence GTC.