Resource Adaptive Agents in Interactive Theorem Proving (2008)
Christoph Benzmuller, Volker Sorge
We introduce a resource adaptive agent mechanism which supports the user in interactive theorem proving. The mechanism, an extension of [4], uses a two layered architecture of agent societies to...
Abstract Agent Based Mathematical Reasoning 1 (2008)
Christoph Benzmuller, Mateja Jamnik, Manfred Kerber, Volker Sorge
In this contribution we propose an agent architecture for theorem proving which we intend to investigate in depth in the future. The work reported in this paper is in an early state, and by no means...
Command Blackboard Command Agents Suggestion Blackboards (2008)
Christoph Benzmuller, Volker Sorge
Agent Based Command Suggestion Mechanism In order to support users within large proofs, most interactive theorem provers have some limited capability to suggest parameters of choosen commands or even...
Strategic Issues Related to the Development and Use of TPS (2007)
Christoph Benzmuller, Volker Sorge, Integrating Tps, Peter Andrews
nsion trees and matings (using ideas described in [1] and [3]), but TPS proofs are presented in natural deduction style, and TPS can operate in a mixture of interactive and automatic modes [6]. Many...
Mathematical domain reasoning tasks in natural language tutorial dialog on proofs (2005)
Benzmuller, Christoph, Vo, Quoc Bao
We study challenges that are imposed to mathematical domain reasoning in the context of natural language tutorial dialog on mathematical proofs. The focus is on proof step evaluation: (i) How can...
Assertion-level proof representation with under-specification (2004)
Autexier, Serge, Benzmuller, Christoph, Fiedler, Armin, Horacek, Helmut, Vo, Bao Quoc
We propose a proof representation format for human-oriented proofs at the assertion level with under-specification. This work aims at providing a possible solution to challenging phenomena worked out...
Proof transformation and expansion with a parameterizable inference machine (2001)
Christoph Benzmuller, Andreas Meier, Martin Pollet, Volker Sorge
or\Omega mega [ 2] provide proof tactics and/or proof methods to support abstract level proof construction and to improve the communication with the user. Tactics and methods typically abbreviate...
Integrating TPS and mega (1999)
Christoph Benzmuller, Matthew Bishop, Volker Sorge
Abstract: This paper reports on the integration of the higher-order theorem proving environment Tps [Andrews et al., 1996] into the mathematical assistant mega [Benzmuller et al., 1997]. Tps can be...
Towards Concurrent Resource Managed Deduction (1999)
Germany Www, Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge, Christoph Benzmuller, ...
In this paper, we describe an architecture for resource guided concurrent mechanised deduction which is motivated by some findings in cognitive science. Its benefits are illustrated by comparing it...
Critical Agents Supporting Interactive Theorem Proving (1999)
Christoph Benzmuller And, Christoph Benzmuller, Volker Sorge
. We introduce a resource adaptive agent mechanism which supports the user of an interactive theorem proving system. The mechanism, an extension of [4], uses a two layered architecture of agent...
Towards Concurrent Resource Managed Deduction (1999)
Christoph Benzmuller Mateja, Christoph Benzmuller, Mateja Jamnik, Mateja Jamnik, Manfred Kerber, Manfred Kerber, ...
In this paper, we describe an architecture for resource guided concurrent mechanised deduction which is motivated by some findings in cognitive science. Its benefits are illustrated by comparing it...
Critical agents supporting interactive theorem proving (1999)
Christoph Benzmuller, Volker Sorge
Abstract. We introduce a resource adaptive agent mechanism which supports the user of an interactive theorem proving system. The mechanism, an extension of [5], uses a two layered architecture of...
Concurrent Resource Managed Theorem Proving (1999)
Christoph Benzmuller, Mateja Jamnik, Manfred Kerber, Volker Sorge, Christoph Benzmuller, ...
In this paper, we describe an architecture for resource guided concurrent mechanised deduction which is motivated by some ndings in cognitive science. Its bene ts are illustrated by comparing it with...
Extensional Higher-Order Resolution (1998)
Christoph Benzmuller And, Christoph Benzmuller, Michael Kohlhase
. 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...
Christoph Benzmuller, Michael Kohlhase
this paper was supported by the Deutsche Forschungsgemeinschaft in grant HOTEL.
Integrating Tps with mega (1998)
Christoph Benzmuller, Volker Sorge
We report on the integration of Tps as an external reasoning component into the mathematical assistant system mega. Thereby Tps can be used both as an automatic theorem prover for higher order logic...
Jorg Siekmann, Stephan Hess, Christoph Benzmuller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, ...
Most interactive proof development environments are insu cient to handle the complexity of the information to be conveyed to the user and to support his orientation in large-scale proofs. In this...
A blackboard architecture for guiding interactive proofs (1998)
Christoph Benzmuller, Volker Sorge
Abstract. The acceptance and usability of current interactive theorem proving environments is, among other things, strongly in uenced by the availability ofanintelligent default suggestion mechanism...
mega: Towards a mathematical assistant (1997)
Christoph Benzmuller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, ...
Abstract. 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...