zbMATH — the first resource for mathematics

A semantic completeness proof for TaMeD. (English) Zbl 1165.68451
Hermann, Miki (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 13th international conference, LPAR 2006, Phnom Penh, Cambodia, November 13–17, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-48281-9/pbk). Lecture Notes in Computer Science 4246. Lecture Notes in Artificial Intelligence, 167-181 (2006).
Summary: Deduction modulo is a theoretical framework designed to introduce computational steps in deductive systems. This approach is well suited to automated theorem proving and a tableau method for first-order classical deduction modulo has been developed. We reformulate this method and give an (almost constructive) semantic completeness proof. This new proof allows us to extend the completeness theorem to several classes of rewrite systems used for computations in deduction modulo. We are then able to build a counter-model when a proof fails for these systems.
For the entire collection see [Zbl 1135.68002].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
68Q42 Grammars and rewriting systems
PDF BibTeX Cite
Full Text: DOI