Superposition with simplification as a decision procedure for the monadic class with equality
- 11 June 2005
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- Ordered paramodulation and resolution as decision procedurePublished by Springer Nature ,1993
- Saturation of first-order (constrained) clauses with the Saturate systemPublished by Springer Nature ,1993
- Resolution Methods for the Decision ProblemPublished by Springer Nature ,1993
- Theorem-proving with resolution and superpositionJournal of Symbolic Computation, 1991
- On restrictions of ordered paramodulation with simplificationPublished by Springer Nature ,1990
- Complexity results for classes of quantificational formulasJournal of Computer and System Sciences, 1980
- Resolution Strategies as Decision ProceduresJournal of the ACM, 1976
- Über Möglichkeiten im RelativkalkülMathematische Annalen, 1915