CADE
2004
Springer
13 years 9 months ago
2004
Springer
The dependency pair approach is one of the most powerful techniques for automated (innermost) termination proofs of term rewrite systems (TRSs). For any TRS, it generates inequalit...
CADE
2004
Springer
13 years 9 months ago
2004
Springer
The paper presents a modular superposition calculus for the combination of first-order theories involving both total and partial functions. Modularity means that inferences are pu...
CADE
2004
Springer
14 years 4 months ago
2004
Springer
LRR [3] is a rewriting system developed at the Computer Science Department of University of Houston. LRR has two subsystems: Smaran (for tabled rewriting), and TGR (for untabled re...
CADE
2004
Springer
14 years 4 months ago
2004
Springer
CADE
2004
Springer
14 years 4 months ago
2004
Springer
CADE
2004
Springer
14 years 4 months ago
2004
Springer
ended abstract motivates and presents techniques for identifying variable independence in free variable calculi for classical logic without equality. Two variables are called indep...
CADE
2004
Springer
14 years 4 months ago
2004
Springer
CADE
2004
Springer
14 years 4 months ago
2004
Springer
This paper is concerned with the integration of recursive data structures with Presburger arithmetic. The integrated theory includes a length function on data structures, thus prov...
CADE
2004
Springer
14 years 4 months ago
2004
Springer
This paper presents the Dr.Doodle system, an interactive theorem prover that uses diagrammatic representations. The assumption underlying this project is that, for some domains (pr...
CADE
2004
Springer
14 years 4 months ago
2004
Springer
The CADE ATP System Competition (CASC) is an annual evaluation of fully automatic, first-order Automated Theorem Proving systems. CASC-18 was the seventh competition in the CASC se...