A method for building models automatically. Experiments with an extension of OTTER
- 1 January 1994
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 11 references indexed in Scilit:
- Superposition with simplification as a decision procedure for the monadic class with equalityPublished by Springer Nature ,2005
- Model building by resolutionPublished by Springer Nature ,1993
- Resolution Methods for the Decision ProblemPublished by Springer Nature ,1993
- A method for simultaneous search for refutations and models by equational constraint solvingJournal of Symbolic Computation, 1992
- Extending resolution for model constructionPublished by Springer Nature ,1991
- Equational problems anddisunificationJournal of Symbolic Computation, 1989
- Empirical Explorations of the Geometry-Theorem Proving MachinePublished by Springer Nature ,1983
- Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open QuestionsJournal of the ACM, 1982
- Decidability of a portion of the predicate calculusIsrael Journal of Mathematics, 1977
- Automatic Theorem Proving With Renamable and Semantic ResolutionJournal of the ACM, 1967