Algorithms, Datastructures, and other Issues in Efficient Automated Deduction
Author:
- 8 June 2001
- book chapter
- Published by Springer Nature in Lecture Notes in Computer Science
- p. 13-28
Abstract
No abstract availableKeywords
This publication has 68 references indexed in Scilit:
- The Automation of Proof by Mathematical Induction2001
- Unification Theory2001
- Resolution Theorem Proving2001
- FDPLL — A First-Order Davis-Putnam-Logeman-Loveland Procedure2000
- System description: Leo — A higher-order theorem proverLecture Notes in Computer Science, 1998
- Extensional higher-order resolutionLecture Notes in Computer Science, 1998
- Avoiding slack variables in the solving of linear diophantine equations and inequationsTheoretical Computer Science, 1997
- DISCOUNT: A system for distributed equational deduction1995
- Associative-commutative discrimination nets1993
- Flatterms, discrimination nets, and fast term rewritingJournal of Automated Reasoning, 1993