A method for simultaneous search for refutations and models by equational constraint solving
- 30 June 1992
- journal article
- Published by Elsevier in Journal of Symbolic Computation
- Vol. 13 (6) , 613-641
- https://doi.org/10.1016/s0747-7171(10)80014-8
Abstract
No abstract availableKeywords
This publication has 12 references indexed in Scilit:
- Solving disequations in equational theoriesPublished by Springer Nature ,2005
- Equational formulas in order-sorted algebrasPublished by Springer Nature ,2005
- A canonical form for generalized linear constraintsJournal of Symbolic Computation, 1992
- User-oriented theorem proving with the ATINF graphic proof editorPublished by Springer Nature ,1991
- Querying constraintsPublished by Association for Computing Machinery (ACM) ,1990
- Equational problems anddisunificationJournal of Symbolic Computation, 1989
- Seventy-five problems for testing automatic theorem proversJournal of Automated Reasoning, 1986
- Equality-based binary resolutionJournal of the ACM, 1986
- Resolution Strategies as Decision ProceduresJournal of the ACM, 1976
- Automatic Theorem Proving With Renamable and Semantic ResolutionJournal of the ACM, 1967