zbMATH — the first resource for mathematics

Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure. (English) Zbl 07178983
Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer (ISBN 978-3-030-29435-9/pbk; 978-3-030-29436-6/ebook). Lecture Notes in Computer Science 11716. Lecture Notes in Artificial Intelligence, 300-318 (2019).
Summary: We propose a lazy decision procedure for the logic \(\mathrm{WS}k\mathrm{S}\). It builds a term-based symbolic representation of the state space of the tree automaton (TA) constructed by the classical \(\mathrm{WS}k\mathrm{S}\) decision procedure. The classical decision procedure transforms the symbolic representation into a TA via a bottom-up traversal and then tests its language non-emptiness, which corresponds to satisfiability of the formula. On the other hand, we start evaluating the representation from the top, construct the state space on the fly, and utilize opportunities to prune away parts of the state space irrelevant to the language emptiness test. In order to do so, we needed to extend the notion of language terms (denoting language derivatives) used in our previous procedure for the linear fragment of the logic (the so-called \(\mathrm{WS}1\mathrm{S}\)) into automata terms. We implemented our decision procedure and identified classes of formulae on which our prototype implementation is significantly faster than the classical procedure implemented in the Mona tool.
For the entire collection see [Zbl 1428.68018].
03B35 Mechanization of proofs and logical operations
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Full Text: DOI