Cut Elimination with ξ-Functionality (2009)
Christoph E. Benzmüller, Chad E. Brown
In this paper we will give a complete, cut-free sequent calculus for a fragment of higher-order logic with ξ-extensionality, a weak form of functional extensionality. When one wants a calculus...
In [1] Andrews studies elementary type theory, a form of Church’s type theory [12] without extensionality, descriptions, choice, and infinity. Since most of the automated search procedures...
Christoph E. Benzmüller, Chad E. Brown, To Andrzej Trybulec
Abstract. We examine Boolos ’ curious inference and formalize it in a system based on set theory (Mizar) and a system based on classical higherorder logic (OMEGA). The Boolos example is interesting...
Cut-Simulation and Impredicativity (2009)
Benzmueller, Christoph, Brown, Chad E., Kohlhase, Michael
We investigate cut-elimination and cut-simulation in impredicative (higher-order) logics. We illustrate that adding simple axioms such as Leibniz equations to a calculus for an impredicative logic --...
Terminating Tableaux for the Basic Fragment of Simple Type Theory (2009)
We consider the basic fragment of simple type theory, which restricts equations to base types and disallows lambda abstractions and quantifiers. We show that this fragment has the finite model...
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...
Truth Through Proof. Kluwer Academic Publishers, second edition, 2002. (2008)
Tps [1, 2] is a theorem proving system providing support for automated and interactive proving in fragments of Church’s Type Theory [3, 5]. Tps has been developed by Peter Andrews and several of...
Benchmarks for Higher-Order Automated Reasoning (2008)
For a higher-order system to be successful it should support users performing tasks both large and small. Large tasks include interactive construction of large theories, including storing...
Cut Elimination with ξ-Functionality (2008)
Christoph E. Benzmüller, Chad E. Brown
In [1] Andrews proved cut-elimination for a sequent calculus G for elementary type theory (Corollary 4.11 there). In particular, Andrews proved provability in G is equivalent to provability in a...
ETPS: A System to Help Students Write Formal Proofs (2008)
Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi
ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in first-order logic or higher-order logic. It enables students to concentrate on the...
ETPS: A System to Help Students Write Formal Proofs (2007)
Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi
ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in rst-order logic or higher-order logic. It enables students to concentrate on the...
The Standard PER Model in the Reynolds/Ma Framework (2007)
The standard PER model of the polymorphic lambda calculus can be realized
The Kolmogorov Interpretation of Classical Logic in Intuitionistic Logic (2007)
We indicate how to represent the Kolmogorov interpretation of classical firstorder logic in intuitionistic first-order logic using the logical framework LF (see [Pfe]). We also implement this...
The Bainbridge-Freyd-Scedrov-Scott Parametric PER Model in the Reynolds/Ma Framework (2007)
In Reynolds and Ma [2], semantics for the polymorphic lambda calculus are given using PL categories. A notion of parametricity is also defined. In Bainbridge, Freyd, Scedrov, and Scott [1], a...
Example: A Standard Frame: (2006)
Christoph Benzmüller, Chad E. Brown
We consider (classical) higher-order logic formulated as Church’s simple type theory [Chu40] based on the simply typed λ-calculus. We first define the set of (simple) types T. Definition 1 (Types)...
Searchable Online Edition (2006)
Dependently Typed Set Theory (DeTSeT) is untyped set theory encoded in a dependent type theory. The dependent type theory includes proof irrelevance and a special Σ-type between objects and proofs....
A Structured Set of Higher-Order Problems (2005)
Christoph E. Benzmüller, Chad E. Brown
Abstract. We present a set of problems that may support the development of calculi and theorem provers for classical higher-order logic. We propose to employ these test problems as quick and easy...
Designing a GUI for Proofs – Evaluation of an HCI Experiment (2005)
Fachrichtung Informatik, Martin Homik, Andreas Meier, Dfki Gmbh Saarbrücken, Chad E. Brown, ...
Often user interfaces of theorem proving systems focus on assisting particularly trained and skilled users, i.e., proof experts. As a result, the systems are difficult to use for non-expert users....
Higher-order semantics and extensionality (2004)
Benzmüller, Christoph, Brown, Chad E., Kohlhase, Michael
In this paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher-order...
Higher-Order Semantics and Extensionality (2004)
Christoph Benzmüller, Chad E. Brown, Michael Kohlhase
Abstract. In this paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of...
ETPS: A System to Help Students Write Formal Proofs (2003)
Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi
ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in first-order logic or higher-order logic. It enables students to concentrate on the...
ETPS: A System to Help Students Write Formal Proofs (2003)
Chad E. Brown, Peter B. Andrews, Peter B. Andrews, Matthew Bishop, Matthew Bishop, Sunil Issar, ...
ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in rst-order logic or higher-order logic. It enables students to concentrate on the...
ETPS: A System to Help Students Write Formal Proofs (2003)
Peter Andrews, Peter B. Andrews, Chad E. Brown, Chad E. Brown, Matthew Bishop, Matthew Bishop, ...
ETPS (Educational Theorem Proving System) is a program which logic students can use to write formal proofs in first-order logic or higher-order logic. It enables students to concentrate on the...
Solving for Set Variables in Higher-Order Theorem Proving (2002)
In higher-order logic, we must consider literals with exible (set variable) heads. Set variables may be instantiated with logical formulas of arbitrary complexity. An alternative to guessing the...