A Structure-preserving Clause Form Translation
- 30 September 1986
- journal article
- Published by Elsevier in Journal of Symbolic Computation
- Vol. 2 (3), 293-304
- https://doi.org/10.1016/s0747-7171(86)80028-1
Abstract
No abstract availableKeywords
This publication has 6 references indexed in Scilit:
- Completely non-clausal theorem provingArtificial Intelligence, 1982
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980
- Simplification by Cooperating Decision ProceduresACM Transactions on Programming Languages and Systems, 1979
- On the SUP-INF Method for Proving Presburger FormulasJournal of the ACM, 1977
- Splitting and reduction heuristics in automatic theorem provingArtificial Intelligence, 1971
- The Concept of Demodulation in Theorem ProvingJournal of the ACM, 1967