Volker Sorge

Database-driven Mathematical Character Recognition (2008)

der Naturwissenschaftlich-Technischen Fakult"at I

Alan Sexton, Volker Sorge

Abstract. We present an approach for recognising mathematical texts using an extensive L ATEX symbol database and a novel recognition algorithm. The process consists essentially of three steps:...

Resource Guided Concurrent Deduction (2008)

Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge

Our poster proposes an architecture for resource guided concurrent mechanised deduction which is motivated by some findings in cognitive science. Our architecture particularly reflects Hadamard’s...

Resource Guided Concurrent Deduction (2008)

Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge

Our poster proposes an architecture for resource guided concurrent mechanised deduction which is motivated by some findings in cognitive science. Our architecture particularly reflects Hadamard’s...

A Grid-based Application of Machine Learning to Model Generation (2008)

Volker Sorge, Simon Colton, Andreas Meier, Roy Mccasl

Abstract. The classification of mathematical structures is a driving force in pure mathematics. A first step in producing algebraic classification theorems is to determine for which sizes certain...

Formal Aspects of Computing (2008)

Jörg Siekmann, Stephan Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Armin Fiedler, Helmut Horacek, ...

Abstract. The capabilities of a automated theorem prover’s interface are essential for the effective use of (interactive) proof systems. LΩUI is the multi-modal interface that combines several...

Austrian Society for Cybernetic Studies, 2004. Representation of Mathematical Concepts for Inferencing and for Presentation Purposes (2008)

Fachrichtung Informatik, Helmut Horacek, Armin Fiedler, Andreas Franke, Markus Moschner, ...

Knowledge bases that represent some domain expertise for use in a formal system typically serve one of two major purposes: (1) inferencing in some problem-solving context, or (2) interfacing the...

Combining Proofs of Higher-Order and First-Order Automated Theorem Provers (2008)

Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber

Abstract. Ωants is an agent-oriented environment for combining inference systems. A characteristics of the Ωants approach is that a common proof object is generated by the cooperating systems....

Planning Equivalence Proofs (2008)

Lassaad Cheikhrouhou, Volker Sorge

Di erent axiomatizations of mathematical concepts prove to be useful in a mathematical knowledge base, since each axiomatization of a concept is more or less helpful for the task at hand. To keep the...

A Grid-based Application of Machine Learning to Model Generation (2008)

Volker Sorge, Simon Colton, Andreas Meier, Roy Mccasl

Abstract. The classification of mathematical structures is a driving force in pure mathematics. A first step in producing algebraic classification theorems is to determine for which sizes certain...

CLASSIFICATION RESULTS IN QUASIGROUP AND LOOP THEORY VIA A COMBINATION OF AUTOMATED REASONING TOOLS (2008)

Volker Sorge, Simon Colton, Roy Mccasland, Andreas Meier

Abstract. We present some novel partial classification results in quasigroup and loop theory. For quasigroups up to size XXX and loops up to size YYY, we describe a unique property which determines...

Database-driven Mathematical Character Recognition (2008)

Alan Sexton, Volker Sorge

We present an approach for recognising mathematical texts using an extensive L ATEX symbol database and a novel recognition algorithm. The process consists essentially of three steps: Recognising the...

Resource Adaptive Agents in Interactive Theorem Proving (2008)

An Implementation of Distributed Mathematical Services (2008)

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...

Stephan M. Hess, Christoph G. Jung, Michael Kohlhase, Volker Sorge

Real-world applications of theorem proving require open and modern software environments that enable modularization, distribution, inter-operability, networking, and coordination. This paper...

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)

Combining AI Systems for Classification in Non-associative Algebra (2008)

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...

Volker Sorge, Andreas Meier

Replace this file with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be found at the ENTCS Macro Home Page.

Abstract Employing External Reasoners in Proof Planning (2008)

Erica Melis, Volker Sorge

This paper describes the integration of computer algebra systems and constraint solvers into proof planners. It shows how e cient external reasoners can be employed in proof planning and how the...

Resource Guided Concurrent Deduction (2008)

Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge

Our poster proposes an architecture for resource guided concurrent mechanised deduction which is motivated by some findings in cognitive science. Our architecture particularly reflects Hadamard’s...

Classes Extended Abstract (2008)

Tactics (2008)

Adaptive Course Generation and Presentation (2008)

Paul Libbrecht, Andreas Meier, Erica Melis, Martin Pollet, Volker Sorge, Carsten Ullrich

1 Introduction Today's interactive mathematics textbooks [4, 5] use a collection of predefined documents including a fixed set of examples and exercises. Neither can the content (e.g., examples...

Agent Based Mathematical Reasoning (2007)

Christoph Benzmuller Mateja, 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...

Agent Based Mathematical Reasoning (2007)

Christoph Benzmuller Mateja, 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...

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...

Integrating TPS with OMEGA (2007)

Resource Guided Concurrent Deduction (2007)

. We report on the integration of Tps as an external reasoning component into the mathematical assistant system\Omega mega. Thereby Tps can be used both as an automatic theorem prover for higher...

Christoph Benzmueller, Mateja Jamnik, Manfred Kerber, Volker Sorge

Our poster proposes an architecture for resource guided concurrent mechanised deduction which is motivated by some findings in cognitive science. Our architecture particularly reflects...

I S (2007)

Armin Fiedler, Xiaorong Huang, Manfred Kerber, Karsten Konrad, Andreas Meier, Erica Melis, ...

at

In (2007)

Exploring the Domain of Residue Classes (2007)

Huang has identied the assertion level as a well dened abstraction level for natural deduction proofs [5, 6]. Proofs at assertion level are composed of the direct application of assertions, like...

Germany Www, U Niv, Andreas Meier, Andreas Meier, Martin Pollet, Martin Pollet, ...

We report on a major case study on combining proof planning with computer algebra systems. We construct proofs for basic algebraic properties of residue classes as well as for isomorphisms between...

Automatically Exploring the Domain of Residue Classes Extended Abstract (2007)

mega User Interface (2007)

We describe a module for exploring simple algebraic properties of operations on residue class sets over the integers. The framework is implemented within

Karsten Konrad, Andreas Meier, Erica Melis, Martin Pollet, Volker Sorge

Abstract. The capabilities of a automated theorem prover's interface are essential for the eective use of (interactive) proof systems. L UI is the multi-modal interface that combines several...

2 (2007)

Andreas Meier, Volker Sorge, Simon Colton

Abstract. The invention of suitable concepts to characterise mathematical structures is one of the most challenging tasks for both human mathematicians and automated theorem provers alike. We present...

A rational reconstruction of a system for experimental mathematics (2007)

AIMSS: An Architecture for Data Driven Simulations (2007)

Over the last decade several environments and formalisms for the combination and integration of mathematical software systems have been proposed. Many of these systems aim at a traditional automated...

Catriona Kennedy, Georgios Theodoropoulos, Volker Sorge, Edward Ferrari, Peter Lee, Chris Skelcher

Abstract. This paper presents a prototype implementation of an intelligent assistance architecture for data-driven simulation specialising in qualitative data in the social sciences. The assistant...

A rational reconstruction of a system for experimental mathematics (2007)

A rational reconstruction of a system for experimental mathematics (2007)

Abstract. In previous papers we described the implementation of a system which combines mathematical object generation, transformation and filtering, conjecture generation, proving and disproving for...

A rational reconstruction of a system for experimental mathematics (2007)

A rational reconstruction of a system for experimental mathematics (2007)

Over the last decade several environments and formalisms for the combination and integration of mathematical software systems have been proposed. Many of these systems aim at a traditional automated...

A rational reconstruction of a system for experimental mathematics (2007)

Abstract. In previous papers we described the implementation of a system which combines mathematical object generation, transformation and filtering, conjecture generation, proving and disproving for...

Managing automatically formed mathematical theories (2006)

Abstract. In previous papers we described the implementation of a system which combines mathematical object generation, transformation and filtering, conjecture generation, proving and disproving for...

Simon Colton, Pedro Torres, Paul Cairns, Volker Sorge

Abstract. The HR system forms scientific theories, and has found particularly successful application in domains of pure mathematics. Starting with only the axioms of an algebraic system, HR can...

Interfacing to computer algebra via term indexing (2006)

Frank Theiß, Volker Sorge, Martin Pollet

this file with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be found at the ENTCS Macro Home Page. blackrgb0,0,0 0.5 setgray0 0.5 setgray1

Towards a parser for mathematical formula recognition (2006)

Amar Raja, Matthew Rayner, Alan Sexton, Volker Sorge

Abstract. For the transfer of mathematical knowledge from paper to electronic form, the reliable automatic analysis and understanding of mathematical texts is crucial. A robust system for this task...

Processing textbook-style matrices (2006)

Alan Sexton, Volker Sorge

Abstract. In mathematical textbooks matrices are often represented as objects of indefinite size containing abbreviations. To make the knowledge implicitly given in these representations available in...

Capturing Abstract Matrices from Paper (2006)

Toshihiro Kanahori, Alan Sexton, Volker Sorge, Masakazu Suzuki

Abstract. Capturing and understanding mathematics from print form is an important task in translating written mathematical knowledge into electronic form. While the problem of syntactically...

Automatic construction and verification of isotopy invariants (2006)

Volker Sorge, Andreas Meier, Roy Mccasl, Simon Colton

Abstract. We extend our previous study of the automatic construction of isomorphic classification theorems for algebraic domains by considering the isotopy equivalence relation, which is of more...

Automatic construction and verification of isotopy invariants (2006)

Automatic construction and verification of isotopy invariants (2006)

Abstract. We extend our previous study of the automatic construction of isomorphic classification theorems for algebraic domains by considering the isotopy equivalence relation. Isotopism is an...

Volker Sorge, Andreas Meier, Roy Mccasl, Simon Colton

Automatic construction and verification of isotopy invariants (2006)

Semantic analysis of matrix structures (2005)

Abstract. We extend our previous study of the automatic construction of isomorphic classification theorems for algebraic domains by considering the isotopy equivalence relation, which is of more...

Alan P. Sexton, Volker Sorge

The automatic interpretation of mathematical text structures has received only limited attention so far. While there has been work on the particularities of the character recognition of two...

Can a higher-order and a first-order theorem prover cooperate (2005)

Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber

Abstract. State-of-the-art first-order automated theorem proving systems have reached considerable strength over recent years. However, in many areas of mathematics they are still a long way from...

LPAR-05 Workshop: Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL) (2005)

Christoph Benzmüller, John Harrison, Carsten Schürmann, Programme Committee, Christoph Kreitz, ...

p.p=A B

Can a higher-order and a first-order theorem prover cooperate (2005)

Volker Sorge, Mateja Jamnik, Manfred Kerber

Database-driven Mathematical Character Recognition (2005)

Alan Sexton And, Alan Sexton, Volker Sorge

We present an approach for recognising mathematical texts using an extensive L T E X symbol database and a novel recognition algorithm. The process consists essentially of three steps: Recognising...

Semantic Analysis of Matrix Structures (2005)

Alan Sexton And, Alan P. Sexton, Volker Sorge

The automatic interpretation of mathematical text structures has received only limited attention so far. While there has been work on the particularities of the character recognition of two...

A new set of algebraic benchmark problems for sat solvers (2005)

Automatic generation of classification theorems for finite algebras (2004)

Solving open quasigroup existence problems is a challenging problem to which SAT solvers have been applied successfully. However, the number of problems of this domain is relatively small and its use...

Simon Colton, Andreas Meier, Volker Sorge, Roy Mccasland

Classifying finite algebraic structures has been a major motivation behind much research in pure mathematics. Automated techniques have aided this process, but this has largely been at a quantitative...

Representation of Mathematical Concepts (2004)

For Inferencing And, Helmut Horacek, Armin Fiedler, Andreas Franke, Markus Moschner, Martin Pollet, ...

Knowledge bases that represent some domain expertise for use in a formal system typically serve one of two major purposes: (1) inferencing in some problem-solving context, or (2) interfacing the...

A Grid-based Application of (2004)

Machine Learning To, Volker Sorge, Simon Colton, Andreas Meier, Roy Mccasl

The classification of mathematical structures is a driving force in pure mathematics. A first step in producing algebraic classification theorems is to determine for which sizes certain algebras...

Intuitive and Formal Representations: The Case of Matrices (2004)

Martin Pollet, Volker Sorge, Manfred Kerber

Abstract. A major obstacle for bridging the gap between textbook mathematics and formalising it on a computer is the problem how to adequately capture the intuition inherent in the mathematical...

Automatic generation of classification theorems for finite algebras (2004)

Simon Colton, Andreas Meier, Volker Sorge, Roy Mccasl

a, b2G a ffi b = b ffi a]. The systemgenerates such results, then proves that they provide valid classifications by showing that each concept is a classifying property, i.e., true for all members of...

Automatic generation of classification theorems for finite algebras (2004)

Simon Colton, Andreas Meier, Volker Sorge

Abstract. Classifying finite algebraic structures has been a major motivation behind much research in pure mathematics. Automated techniques have aided in this process, but this has largely been at a...

First Workshop on Challenges and Novel Applications for Automated Reasoning (2003)

Organisers Simon Colton, Jeremy Gow, Volker Sorge, Toby Walsh

The aim of the workshop was to identify challenges for automated reasoning that will fire both the imaginations of new researchers and those long established in the field. The workshop encompassed...

Certifying solutions to permutation group problems (2003)

Arjeh Cohen, Scott H. Murray, Martin Pollet, Volker Sorge

Abstract. We describe the integration of permutation group algorithms with proof planning. We consider eight basic questions arising in computational permutation group theory, for which our code...

Proof Development with Ωmega (2002)

Jörg Siekmann, Christoph Benzmüller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke, ...

deduction (ND) variant of a sorted version of Church's simply typed #-calculus [8]. The user can interactively construct proofs directly at the calculus level or at the more abstract level of...

Employing theory formation to guide proof planning (2002)

Andreas Meier, Volker Sorge, Simon Colton

Proof Development with OMEGA (2002)

Jörg Siekmann, Christoph Benzmüller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke, ...

e number of dierent reasoning systems and to integrate their results into a single proof structure, (2) support for interactive proof development through some non-standard inspection facilities and...

Employing Theory Formation to Guide Proof Planning (2002)

Andreas Meier, Volker Sorge, Simon Colton

The invention of suitable concepts to characterise mathematical structures is one of the most challenging tasks for both human mathematicians and automated theorem provers alike. We present an...

Article Submitted to Journal of Symbolic Computation (2002)

Comparing Approaches To, Andreas Meier, Martin Pollet, Volker Sorge

We report on a case study on combining proof planning with computer algebra systems. We construct proofs for basic algebraic properties of residue classes as well as for isomorphisms between residue...

Proof Development with ΩMEGA (2002)

Jörg Siekmann, Christoph Benzmüller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke, ...

The OMEGA proof development system [2] is the core of several related and well integrated...

Experiments with an Agent-oriented Reasoning System (2001)

Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge

Abstract. This paper discusses experiments with an agent oriented approach to automated and interactive reasoning. The approach combines ideas from two subfields of AI (theorem proving/proof planning...

Classifying Isomorphic Residue Classes (2001)

Andreas Meier, Martin Pollet, Volker Sorge

Abstract. We report on a case study on combining proof planning with computer algebra systems. We construct proofs for basic algebraic properties of residue classes as well as for isomorphisms...

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...

Proof planning: A fresh start (2001)

Andreas Meier, Erica Melis, Martin Pollet, Volker Sorge

Abstract. Proof Planning is a technique for automated (and interactive) methods. Proof methods consist of a chunk of mathematically motivated, recurring patterns of calculus level inferences with...

Proof Planning: A Fresh Start? (2001)

Christoph Benzm Uller, Andreas Meier, Erica Melis, Martin Pollet, Volker Sorge

Proof Planning is a technique for automated (and interactive) theorem proving that searches for proof plans at the level of abstract methods. Proof methods consist of a chunk of mathematically...

Experiments with an Agent-oriented Reasoning System (2001)

Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge

This paper discusses experiments with an agent oriented approach to automated and interactive reasoning. The approach combines ideas from two sub elds of AI (theorem proving/proof planning and...

Exploring Properties of Residue Classes (2000)

Adaptive Course Generation and Presentation (2000)

Abstract. We report on an experiment in exploring properties of residue classes over the integers with the combined eort of a multi-strategy proof planner and two computer algebra systems. An...

Christoph Benzmüller, Armin Fiedler, Andreas Franke, George Goguadze, Helmut Horacek, ...

Today's interactive mathematics textbooks use a collection of predefined documents, typically organized as a network of HtML pages. This makes a reuse and a sound re-combination of the encoded...

Resource Guided Concurrent Deduction (2000)

Christoph Benzmüller, Christoph Benzm Uller, Mateja Jamnik, Manfred Kerber, Volker Sorge

applied. While this is a successful and appropriate approximation for many tasks (in particular for well understood domains), it seems to have some limitations, which can be better captured by an...

Omega-ANTS - An open approach at combining Interactive and Automated Theorem Proving (2000)

Resource Guided Concurrent Deduction (2000)

. We present the -Ants theorem prover that is built on top of an agent-based command suggestion mechanism. The theorem prover inherits benecial properties from the underlying suggestion mechanism...

Christoph Benzmüller, Christoph Benzm Uller, Mateja Jamnik, Manfred Kerber, Volker Sorge

d and applied. While this is a successful and appropriate approximation for many tasks (in particular for well understood domains), it seems to have some limitations, which can be better captured by...

PDS -- A Three-Dimensional Data Structure for Proof Plans (2000)

Lassaad Cheikhrouhou, Volker Sorge

We present a new data structure that enables to store three-dimensional proof objects in a proof development environment. The aim is to handle calculus level proofs as well as abstract proof plans...

Non-trivial Symbolic Computations in Proof Planning (2000)

Specialized External Reasoners in Proof Planning (2000)

We discuss a pragmatic approach to integrate computer algebra into proof planning. It is based on the idea to separate computation and verification and can thereby exploit the fact that many...

U Niv, Erica Melis, Volker Sorge

This paper describes the integration of efficient external reasoners into proof planning. It shows how computer algebra systems and constraint solvers can be integrated, how the shortcuts produced by...

Non-Trivial Symbolic Computations in Proof Planning (2000)

Integrating TPS and mega (1999)

Abstract. We discuss a pragmatic approach tointegrate computer algebra into proof planning. It is based on the idea to separate computation and veri cation and can thereby exploit the fact that many...

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...

Agent-oriented integration of distributed mathematical services (1999)

Andreas Franke, Stephan M. Hess, Christoph G. Jung, Michael Kohlhase, Volker Sorge

Abstract: Real-world applications of automated theorem proving require modern software environments that enable modularisation, networked inter-operability, robustness, and scalability. These...

Agent-oriented integration of distributed mathematical services (1999)

Andreas Franke, Stephan M. Hess, Christoph G. Jung, Michael Kohlhase, Volker Sorge

Abstract: Real-world applications of automated theorem proving require modern software environments that enable modularisation, networked inter-operability, robustness, and scalability. These...

Towards Concurrent Resource Managed Deduction (1999)

Christoph Benzmüller, Mateja Jamnik, Mateja Jamnik, Manfred Kerber, Manfred Kerber, Volker Sorge, ...

In this paper, we describe an architecture for resource guided concurrent mechanised deduction which is motivated by some ndings in cognitive science. Its benets are illustrated by comparing it with...

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)

Resource Adaptive Agents in Interactive Theorem Proving (1999)

. 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 agent...

Agent Based Mathematical Reasoning (1999)

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...

Christoph Benzmüller, 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...

LOmegaUI: Lovely OMEGA User Interface (1999)

Jörg Siekmann, Stephan Hess, Michael Kohlhase, Christoph Benzmüller, Lassaad Cheikhrouhou, Armin Fiedler, ...

. The capabilities of a theorem proving interface are essential for the effective use of (interactive) proof systems. L UI is the multi-modal interface that combines several features: a graphical...

LOmegaUI: Lovely OMEGA User Interface (1999)

Jörg Siekmann, Stephan Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Armin Fiedler, Helmut Horacek, ...

. The capabilities of a automated theorem prover's interface are essential for the effective use of (interactive) proof systems. L\Omega UI is the multi-modal interface that combines several...

Towards Fine-Grained Proof Planning with Critical Agents (1999)

Christoph Benzmüller, Volker Sorge, H Hy

,u:L 1 ) (s:L 2 ,u:L 1 ,pl:(1)) : : : goal is HO goal is HO goal is HO message: goal is HO Classif. Agent Figure 1: The two layered suggestion mechanism. We have developed a mechanism that suggests...

Employing External Reasoners in Proof Planning (1999)

Erica Melis, Volker Sorge

This paper describes a the integration of computer algebra systems and constraint solvers into proof planners. It shows how efficient external reasoners can be employed in proof planning and how the...

Critical agents supporting interactive theorem proving (1999)

Concurrent Resource Managed Theorem Proving (1999)

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...

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...

Agent-oriented integration of distributed mathematical services (1999)

Andreas Franke, Stephan M. Hess, Christoph G. Jung, Michael Kohlhase, Volker Sorge

Abstract: Real-world applications of automated theorem proving require modern software environments that enable modularisation, networked inter-operability, robustness, and scalability. These...

A blackboard architecture for guiding interactive proofs (1998)

Integrating Computer Algebra Into Proof Planning (1998)

Abstract. The acceptance and usability of current interactive theorem proving environments is, among other things, strongly influenced by the availability of an intelligent default suggestion...

A Blackboard Architecture for Guiding Interactive Proofs (1998)

Abstract. Mechanised reasoning systems and computer algebra systems have different objectives. Their integration is highly desirable, since formal proofs often involve both of the two different...

An Implementation of Distributed Mathematical Services (1998)

. The acceptance and usability of current interactive theorem proving environments is, among other things, strongly influenced by the availability of an intelligent default suggestion mechanism for...

Stephan Hess, Christoph G. Jung, Michael Kohlhase, Volker Sorge

Real-world applications of theorem proving require open and modern software environments that enable modularization, distribution, inter-operability, networking, and coordination. This paper...

Planning Equivalence Proofs (1998)

Lassaad Cheikhrouhou, Volker Sorge

Different axiomatizations of mathematical concepts prove to be useful in a mathematical knowledge base, since each axiomatization of a concept is more or less helpful for the task at hand. To keep...

LOmegaUI: A Distributed Graphical User Interface for the Interactive Proof System OMEGA (1998)

Jörg Siekmann, Stephan Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, ...

Most interactive proof development environments are insufficient to handle the complexity of the information to be conveyed to the user and to support his orientation in large-scale proofs. In this...

Integrating TPS with OMEGA (1998)

LOmegaUI: Lovely OMEGA User Interface (1998)

We report on the integration of Tps as an external reasoning component into the mathematical assistant system\Omega mega. Thereby Tps can be used both as an automatic theorem prover for higher order...

Jörg Siekmann, Stephan M. Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Armin Fiedler, Helmut Horacek, ...

The capabilities a theorem proving interface exhibits are essential for the effective use of proof systems. To date, most interactive proof development environments are still inadequate to handle the...

An Implementation of Distributed Mathematical Services (1998)

Stephan M. Hess, Christoph G. Jung, Michael Kohlhase, Volker Sorge

Real-world applications of theorem proving require open and modern software environments that enable modularization, distribution, inter-operability, networking, and coordination. This paper...

Integrating Computer Algebra Into Proof Planning (1998)

Integrating Tps with mega (1998)

. Mechanised 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,...

L\Omega UI: A Distributed Graphical User Interface for the Interactive Proof System\Omega mega. Submitted to the International Workshop on User Interfaces for Theorem Provers (1998)

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)

Computational Theories - A First Attempt (1997)

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...

OMEGA: Towards a Mathematical Assistant (1997)

In this note we report on some shortcomings in the current theory structures of the \Omega mega database. With the present approach of statically defining axioms and signatures inside theories the...

Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, ...

.\Omega 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...

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...

An Integration of Mechanised Reasoning Computer Algebra that Respects Explicit Proofs (1996)

Manfred Kerber Michael, Manfred Kerber, Michael Kohlhase, Michael Kohlhase, Volker Sorge, Volker Sorge, ...

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...

An Integration of Mechanised Reasoning and Computer Algebra that Respects Explicit Proofs (1996)

Germany Www, Manfred Kerber, Manfred Kerber, Michael Kohlhase, Michael Kohlhase, Volker Sorge, ...

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...

Integrating Computer Algebra with Proof Planning (1996)

Towards a Translation of Computer Algebra Algorithms into Tactics (1996)

. 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...

Integrating Computer Algebra with Proof Planning (1996)

CAS 2 Abstract CAS 1 Function Mappings tactics plan result call Translator Interface Tactic Generator result call Figure 1: System architecture of sapper Unlike other proof planners a CAS does not...

Manfred Kerber, Manfred Kerber, Michael Kohlhase, Michael Kohlhase, Volker Sorge, Volker Sorge

. 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...

An integration of mechanised reasoning and computer algebra that respects explicit proofs (1996)

Manfred Kerber, Manfred Kerber, Michael Kohlhase, Michael Kohlhase, Volker Sorge, Volker Sorge, ...

Mechanised reasoning systems and computer algebra systems have apparently di erent objectives. Their integration is, however, highly desirable, since in many formal proofs both of the two di erent...

Integrating computer algebra with proof planning (1996)