Integrating equational reasoning into instantiation-based theorem proving. (English) Zbl 1095.68111
Marcinkowski, Jerzy (ed.) et al., Computer science logic. 18th international workshop, CSL 2004, 13th annual conference of the EACSL, Karpacz, Poland, September 20–24, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23024-6/pbk). Lecture Notes in Computer Science 3210, 71-84 (2004).
Summary: In this paper we present a method for integrating equational reasoning into instantiation-based theorem proving. The method employs a satisfiability solver for ground equational clauses together with an instance generation process based on an ordered paramodulation type calculus for literals. The completeness of the procedure is proved using the the model generation technique, which allows us to justify redundancy elimination based on appropriate orderings.
For the entire collection see [Zbl 1060.68004].
For the entire collection see [Zbl 1060.68004].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B35 | Mechanization of proofs and logical operations |
