Combining Enumeration and Deductive Techniques in order to Increase the Class of Constructible Infinite Models
- 1 February 2000
- journal article
- Published by Elsevier in Journal of Symbolic Computation
- Vol. 29 (2) , 177-211
- https://doi.org/10.1006/jsco.1999.0360
Abstract
No abstract availableKeywords
This publication has 16 references indexed in Scilit:
- Decision procedures and model building in equational clause logicLogic Journal of the IGPL, 1998
- A New Technique for Verifying and Correcting Logic ProgramsJournal of Automated Reasoning, 1997
- Hyperresolution and automated model buildingJournal of Logic and Computation, 1996
- MODEL FINDING IN SEMANTICALLY GUIDED INSTANCE-BASED THEOREM PROVINGFundamenta Informaticae, 1994
- A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational ProblemsJournal of Logic and Computation, 1993
- An optimality result for clause form translationJournal of Symbolic Computation, 1992
- A method for simultaneous search for refutations and models by equational constraint solvingJournal of Symbolic Computation, 1992
- Equational problems anddisunificationJournal of Symbolic Computation, 1989
- The unsolvability of the Gödel class with identityThe Journal of Symbolic Logic, 1984
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960