Variable elimination and chaining in a resolution-based prover for inequalities
- 1 January 1980
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 5 references indexed in Scilit:
- A Practical Decision Procedure for Arithmetic with Function SymbolsJournal of the ACM, 1979
- A simplifier based on efficient decision algorithmsPublished by Association for Computing Machinery (ACM) ,1978
- A Complete Unification Algorithm for Associative-Commutative FunctionsPublished by Defense Technical Information Center (DTIC) ,1975
- Experiment with an automatic theorem-prover having partial ordering inference rulesCommunications of the ACM, 1973
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965