25 search results - page 3 / 5 » cade 2004 |
CADE
2004
Springer
14 years 5 months ago
2004
Springer
We show how well-known refinements of ordered resolution, in particular redundancy elimination and ordering constraints in combination with a selection function, can be used to obt...
CADE
2004
Springer
14 years 5 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 5 months ago
2004
Springer
Interactive theorem provers can model complex systems, but require much effort to prove theorems. Resolution theorem provers are automatic and powerful, but they are designed to be...
CADE
2004
Springer
14 years 5 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 5 months ago
2004
Springer
Abstract. Undefined terms are commonplace in mathematics, particularly in calculus. The traditional approach to undefinedness in mathematical practice is to treat undefined terms a...