94 Result(s)
within
Chapter
Michael Kohlhase
Mathematical Logic and Formal Languages
-
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
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...
-
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...
-
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...
-
Chapter and Conference Paper
System Description: MBase, an Open Mathematical Knowledge Base
In this paper we describe the MBase system, a web-based, distributed mathematical knowledge base. This system is a mathematical service in MathWeb that offers a universal repository of formalized mathematics wher...
-
Chapter and Conference Paper
OMDoc: Towards an Internet Standard for the Administration, Distribution, and Teaching of Mathematical Knowledge
In this paper we present an extension OMDoc to the Open- Math standard that allows the representation of the semantics and structure of various kinds of mathematical documents, including articles, textbooks, i...
-
Chapter and Conference Paper
System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning
Automated reasoning systems have reached a high degree of maturity in the last decade. Many reasoning tasks can be delegated to an automated theorem prover (ATP) by encoding them into its interface logic, simp...
-
Chapter and Conference Paper
Proof Development with Ωmega
The Ωmega proof development system [2] is the core of several related and well integrated research projects of the Ωmega research group.
-
Chapter and Conference Paper
Towards Collaborative Content Management and Version Control for Structured Mathematical Knowledge
We propose an infrastructure for collaborative content management and version control for structured mathematical knowledge. This will enable multiple users to work jointly on mathematical theories with minima...
-
Chapter
Appendix
In this appendix, we document the changes of the OMDoc format over the versions, provide quick reference tables, and discuss the validation helps.
