Some Useful Commands in TPS (2008)
Peter B. Andrews, Peter B. Andrews, Eve Longini Cohen, Dale A. Miller, Ph. D, Dan Nesmith, ...
[ ∼ A] means “A is not true”; [A ∧ B] means “A and B”; [A ∨ B] means “A or B”; [A ⊃ B] means “A implies B”; [A ≡ B] means “A if and only if B”; When the relative scopes...
TPS: A Theorem Proving Systemfor Classical Type Theory (2008)
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi
AbstractThis is a description of T PS, a theorem proving system for classical type theory (Church's typedl-calculus). T PS has been designed to be a general research tool for manipulating wffs...
Xiaorong Huang, Xiaorong Huang, Manfred Kerber, Manfred Kerber, Michael Kohlhase, Michael Kohlhase, ...
Mathematics generally enjoys the prestige of being the correct scientific discipline par excellence. This reputation comes from the requirement that every claim must be justified by a rigorous proof....
Die Beweisentwicklungsumgebung Omega-MKRK (2000)
Kerber, Manfred, Huang, Xiaorong, Kohlhase, Michael, Melis, Erica, Nesmith, Dan, Richts, Jörn, ...
Die Beweisentwicklungsumgebung Omega-Mkrp soll Mathematiker bei einer ihrer Haupttätigkeiten, nämlich dem Beweisen mathematischer Theoreme unterstützen. Diese Unterstützung muß so komfortabel...
A Test for Evaluating the Practical Usefulness of Deduction Systems (2000)
Kerber, Manfred, Huang, Xiaorong, Kohlhase, Michael, Nesmith, Dan, Richts, Jörn
OMEGA MKRP - A Proof Development Environment (2000)
Huang, Xiaorong, Kerber, Manfred, Kohlhase, Michael, Melis, Erica, Nesmith, Dan, Richts, Jörn, ...
This report presents the main ideas underlyingtheOmegaGamma mkrp-system, an environmentfor the development of mathematical proofs. The motivation for the development ofthis system comes from our...
An Application of Klop's Counterexample to a Higher-Order Rewrite System (2000)
In 1978, Klop demonstrated that a rewrite system constructed by adding the untyped lambda calculus, which has the Church-Rosser property, to a Church-Rosser first-order algebraic rewrite system may...
tps: A theorem proving system for classical type theory (1996)
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi
This is a description of TPS, a theorem proving system for classical type theory (Church’s typed λ-calculus). TPS has been designed to be a general research tool for manipulating wffs of first-...
Ω-MKRP - A Proof Development Environment (1994)
Manfred Kerber, Erica Melis, Xiaorong Huang, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, ...
Introduction In the following we describe the basic ideas underlying\Omega\Gamma mkrp, an interactive proof development environment [6]. The requirements for this system were derived from our...
TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory (1994)
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi, ...
This is a demonstration of TPS, a theorem proving system for classical type theory (Church's typed l-calculus). TPS can be used interactively or automatically, or in a combination of these...
Mkrp Proof, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, ...
This report presents the main ideas underlying the\Omega\Gamma mkrp-system, an environment for the development of mathematical proofs. The motivation for the development of this system comes from our...
Ω-MKRP - A Proof Development Environment (1994)
Xiaorong Huang, Xiaorong Huang, Manfred Kerber, Manfred Kerber, Michael Kohlhase, Michael Kohlhase, ...
Introduction In the following we describe the basic ideas underlying\Omega\Gamma mkrp, an interactive proof development environment [4]. The requirements for this system were derived from our...
An Application of Klop's Counterexample to a Higher-Order Rewrite System (1994)
Germany Www, Dan Nesmith, Dan Nesmith
In 1978, Klop demonstrated that a rewrite system constructed by adding the untyped lambda calculus, which has the Church-Rosser property, to a Church-Rosser first-order algebraic rewrite system may...
TPS: A Theorem Proving System for Classical Type Theory (1994)
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi
This is a description of TPS, a theorem proving system for classical type theory (Church's typed l-calculus). TPS has been designed to be a general research tool for manipulating wffs of first-...
Omega-MKRP - A Proof Development Environment (1992)
Xiaorong Huang, Xiaorong Huang, Manfred Kerber, Manfred Kerber, Michael Kohlhase, Michael Kohlhase, ...
This report presents the main ideas underlying the\Omega\Gamma mkrp-system, an environment for the development of mathematical proofs. The motivation for the development of this system comes from our...
An Application of Klop's Counterexample to a Higher-Order Rewrite System (1989)
In 1978, Klop demonstrated that a rewrite system constructed by adding the untyped lambda calculus, which has the Church-Rosser property, to a Church-Rosser first-order algebraic rewrite system may...
Xiaorong Huang Manfred, Xiaorong Huang, Manfred Kerber, Manfred Kerber, Michael Kohlhase, Michael Kohlhase, ...
This contribution presents the main ideas underlying the\Omega\Gamma mkrp-system, an environment for the development of mathematical proofs. The motivation for the development of this system comes...
KEIM: A Toolkit for Automated Deduction
Manfred Kerber, Erica Melis, Xiaorong Huang, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, ...
. KEIM is a collection of software modules, written in Common Lisp with CLOS, designed to be used in the implementation of automated reasoning systems. KEIM is intended to be used by those who want...