Advertisement
Published in:
2015 | OriginalPaper | Chapter
Reasoning on Schemas of Formulas: An Automata-Based Approach
Author : Nicolas Peltier
Published in: Language and Automata Theory and Applications
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We present a new proof procedure for reasoning on schemas of formulas defined over various (decidable) base logics (e.g. propositional logic, Presburger arithmetic etc.). Such schemas are useful to model sequences of formulas defined by induction on some parameter. The approach works by computing an automaton accepting exactly the values of the parameter for which the formula is satisfiable. Its main advantage is that it is completely modular, in the sense that external tools are used as “black boxes” both to reason on base formulas and to detect cycles in the proof search. This makes the approach more efficient and scalable than previous attempts. Experimental results are presented, showing evidence of the practical interest of the proposed method.