-
Chapter and Conference Paper
Unification in order-sorted type theory
The introduction of sorts to first-order automated deduction has brought a considerable gain in efficiency by reducing the search space. It is therefore promising to treat sorts in higher order theorem proving...
-
Chapter and Conference Paper
Adapting methods to novel tasks in proof planning
In this paper we generalize the notion of method for proof planning. While we adopt the general structure of methods introduced by Alan Bundy, we make an essential advancement in that we strictly separate the ...
-
Chapter and Conference Paper
Ω-MKRP: A proof development environment
-
Chapter and Conference Paper
KEIM: A toolkit for automated deduction
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 to build or u...
-
Chapter and Conference Paper
Unification in a sorted λ-calculus with term declarations and function sorts
The introduction of sorts to first-order automated deduction has brought greater conciseness of representation and a considerable gain in efficiency by reducing search spaces. This suggests that sort informati...
-
Chapter and Conference Paper
Unification in an extensional lambda calculus with ordered function sorts and constant overloading
We develop an order-sorted higher-order calculus suitable for automatic theorem proving applications by extending the extensional simply typed lambda calculus with a higher-order ordered sort concept and const...
-
Chapter and Conference Paper
A mechanization of strong Kleene logic for partial functions
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 account of partial functions usi...
-
Chapter and Conference Paper
Higher-order tableaux
Even though higher-order calculi for automated theorem proving are rather old, tableau calculi have not been investigated yet. This paper presents two free variable tableau calculi for higher-order logic that ...
-
Chapter and Conference Paper
Integrating computer algebra with proof planning
Mechanised reasoning systems and computer algebra systems have apparently different objectives. Their integration is, however, highly desirable, since in many formal proofs both of the two different tasks, pro...
-
Chapter and Conference Paper
A Tableau Calculus for Partial Functions
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 account of partial functions usi...
-
Article
Die Beweisentwicklungsumgebung \(\Omega\) -Mkrp
Die Beweisentwicklungsumgebung \(\Omega\) -Mkrpsoll Mathematiker bei einer ihrer Haupttätigkeiten, nämlich dem Beweisen mathematischer Theoreme unterstützen. Diese Unterstützung ...
-
Chapter and Conference Paper
Mechanising partiality without re-implementation
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 account of partial functions usi...
-
Chapter and Conference Paper
Ωmega: Towards a mathematical assistant
Ωmega is a mixed-initiative system with the ultimate purpose of supporting theorem proving in main-stream mathematics and mathematics education. The current system consists of a proof planner and an integrated co...
-
Chapter and Conference Paper
A colored version of the λ-calculus
Rippling is a technique developed for inductive theorem proving which uses syntactic differences of terms to guide the proof search. Annotations (like colors) to terms are used to maintain this information. Th...
-
Chapter and Conference Paper
System description: Leo — A higher-order theorem prover
-
Chapter and Conference Paper
Extensional higher-order resolution
In this paper we present an extensional higher-order resolution calculus that is complete relative to Henkin model semantics. The treatment of the extensionality principles — necessary for the completeness res...
-
Article
Ωmega: Ein mathematisches Assistenzsystem
Ωmega is a deduction system for the mathematical practice and mathematics education. The underlying vision is that of an automated mathematical assistant that supports the working mathematician in many tasks. ...
-
Article
Steuerung der Inferenz in der Diskursverarbeitung
Semantic interpretation is an essential component of natural language understanding, which draws on extremely efficient language-based inference techniques. Such techniques are still lacking in computational s...
-
Article
Integrating Computer Algebra into Proof Planning
Mechanized reasoning systems and computer algebra systems have different objectives. Their integration is highly desirable, since formal proofs often involve both of the two different tasks proving and calcula...
-
Chapter and Conference Paper
System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving
Real-world applications of theorem proving require open and modern software environments that enable modularization, distribution, inter-operability, networking, and coordination. This system description prese...
