CADE
1994
Springer
13 years 8 months ago
1994
Springer
CADE
1994
Springer
13 years 8 months ago
1994
Springer
In this paper we investigate the concept of simple termination. A term rewriting system is called simply terminating if its termination can be proved by means of a simpli cation o...
CADE
1994
Springer
13 years 8 months ago
1994
Springer
Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic acc...
CADE
1994
Springer
13 years 8 months ago
1994
Springer
CADE
1994
Springer
13 years 8 months ago
1994
Springer
This paper introduces the imps proof script mechanism and some practical methods for exploiting it.
CADE
1994
Springer
13 years 8 months ago
1994
Springer
Pi is a system for the interactive construction and editing of formal derivations in the calculus of finitary partial inductive definitions. This calculus can be used as a logical ...
CADE
1994
Springer
13 years 8 months ago
1994
Springer
We present a completion-based method for handling a new version of E-unification, called "mixed" E-unification, that is a combination of the classical "universal&quo...
CADE
1994
Springer
13 years 8 months ago
1994
Springer
CADE
1994
Springer
13 years 8 months ago
1994
Springer
Abstract. PROTEIN (PROver with a Theory Extension INterface) is a PTTPbased first order theorem prover over built-in theories. Besides various standardrefinements knownformodelelim...
CADE
1997
Springer
13 years 9 months ago
1997
Springer