Agent-Oriented Theorem Proving

EPSRC Grant: GR/M99644/01 - Review Report

Christoph Benzmüller, Mateja Jamnik, Manfred Kerber
School of Computer Science, The University of Birmingham
Birmingham B15 2TT, England
{C.E.Benzmuller|M.Jamnik|M.Kerber}@cs.bham.ac.uk
http://www.cs.bham.ac.uk/~mmk/projects/AOTP/index.html

Background/Context

The project applies the multi-agent paradigm to theorem proving. A key idea is to view external reasoning systems as autonomous agents making contributions to a centralized proof attempt and to guide their computations by resource management.

A key aspect of the project is to re-use existing reasoning systems (like existing first-order and higher-order theorem provers). We do not address communication issues in this project, since for these we employ the existing mathematical softwarebus (a uniform internet-based interface for connecting reasoning tools). Using this technology, we developed in this project an approach to cooperative building of mathematical proofs.

The integration of heterogenous reasoning systems is internationally recognised as an important next step in the development of automated reasoning systems. It is funded for instance, in the EU-funded Research Training Network (Fifth Framework), Calculemus.

   
Key Advances and Supporting Methodology

The last decade has seen a development of various reasoning systems which are specialised in specific problem domains. Theorem proving contests, such as the annual CASC competition, have shown that these systems typically perform well in their particular niches but often do poorly in others, or are not even applicable outside their specific niche. Whereas many hard-wired integrations of reasoning systems have been shown to be fruitful rather few architectures have been discussed so far that try to overcome the limitations of single reasoning systems by a flexible integration.

In this project we have investigated an approach to integrating heterogeneous kinds of reasoning agents which work for specialised higher-order and first-order theorem provers, natural deduction style theorem provers, model generators, computer algebra systems, etc. The long term goal is to widen the range of mechanisable mathematics by allowing a flexible cooperation between specialist systems. This seems to be best achieved by an agent-based approach for a number of reasons. Firstly, from a software engineering point of view it offers a flexible way to integrate systems. Secondly, and more importantly, the agent-oriented approach allows for flexible proof search. This means that each single system - in form of an agent - can focus on parts of the problem it is good at, without the need to specify a priori a hierarchy of calls. By the agent approach it is possible to overcome many limitations of static and hard-wired integrations. Furthermore the agent based framework helps us to desequentialise and distribute conceptually independent reasoning processes as much as possible. An advantage of our approach to hard-wired integrations or even re-implementations of specialised reasoners is that it makes the reuse of existing systems possible (even without the need for a local installation of these systems). Accessing external systems is orchestrated by packages like  [Franke et al.1999] or the logic broker architecture [Armando and Zini2000]. From the perspective of these infrastructure packages our work can be seen as an attempt to make strong use of their system distribution features.

Related agent-based theorem proving systems [Denzinger and Fuchs1999,Fisher and Ireland1998,Wolf1998,Fisher1997,Denzinger et al.1997] have demonstrated the feasibility and usefulness of agent oriented theorem proving. Our approach differs from previous work in various aspects. The main difference is that we are interested in combining heterogeneous systems, while we want to maintain a uniform representation of the overall proof attempt in natural deduction style. The proof results are explicitly represented in the core system in a higher-order natural deduction calculus. The core system is built on top of a proof development environment and its logic is a (sorted) higher-order logic based on Church's simply typed $\lambda$-calculus. If full natural deduction translation packages for integrated reasoners are available, then the proof contributions of these systems can be verified in the core system. In case they are not available, then we choose ad hoc representations and trust that these systems are correct. However, in contrast to several other researchers we believe that trust is not enough and in the long run we aim at adding further translation mappings for external reasoners. Translating or representing external results in a uniform core system has also advantages with respect to the human-computer interface. Instead of dealing with several representation formalisms our approach enables the user to analyse and select contributions of external reasoners in the natural deduction calculus of the core system.

Our system currently uses about one hundred agents. They are split in several agent societies where each society is associated with one natural deduction rule/tactic of the base calculus. This agent set is extended by further agents encapsulating external reasoners. The encapsulation may be a direct one in case of locally installed external systems, or an indirect one via the framework, which facilitates their distribution over the internet. Employing numerous agents, amongst them powerful theorem provers which are computationally expensive, requires sufficient computation resources. Hence, it is crucial to build the whole system in a customisable and resource adaptive way. The former is achieved by providing a declarative agent specification language and mechanisms supporting the definition, addition, or deletion of reasoning agents (as well as some other proof search critical components and heuristics) even at run-time. For the latter, the agents in our framework can monitor their own performance, can adapt their capabilities, and can communicate to the rest of the system their corresponding resource information. This enables explicit resource reasoning, facilitated by a specialised resource agent, and provides the basic structures for resource adaptive theorem proving. The rest of the section is structured as follows: subsection 2.1 presents the main components of the system architecture. Experiments with the architecture are sketched in subsection 2.2.

System Architecture

The current system architecture is depicted in Figure 1. The core of the system is written in Allegro Common Lisp and employs its multi-processing facilities. Its main components and their particular tasks are described here.

Initial problems, partial proofs as well as completed proofs are represented in the proof data structure and the natural deduction infrastructure provided by the core system,  [Omega Group1997].

Our approach builds on the reactive suggestion mechanism  [Benzmüller and Sorge2000] as a reactive, resource adaptive basis layer of our framework. Triggered by changes in the proof data structure this mechanism dynamically computes applicable commands with their particular parameter instantiations and calls external reasoners into the current proof state. An important aspect is that all agent computations in this mechanism are de-sequentialised and distributed. The idea of this reactive layer is to receive results of inexpensive computations (e.g., the applicability of natural deduction rules) quickly while external reasoners search for their respective proof steps within the limits of their available resources, until a suggested command is selected and executed. A special resource agent may receive performance data from self-monitoring agents in order to adjust the system at run time. Heuristic criteria are used to dynamically filter and sort the list of generated suggestions. They are then passed to the selector and/or the user. Agents as well as heuristic criteria can be added/deleted/modified at run time.

 

  

Figure 1: System architecture. 

provides agents for the basic natural deduction calculus computations. It also provides agents invoking additional proof tactics/methods and external reasoning systems. The latter are called indirectly via the system. We have extended the approach from [Benzmüller and Sorge2000] in the context of our work to be able to integrate partial proofs as results from the external reasoning systems into the overall proof as well as to store different alternative subproofs simultaneously. This also resulted in more complex heuristics to choose among several automatically generated partial proofs. Moreover, we extended 's graphical user interface to be able to display different subproofs of external reasoners as choices for the user.

The Mathweb system realises calls to external reasoners which may be distributed over the internet. In our most recent experiments we tested the new ONE- system which is based on a multi-broker architecture. Each broker has knowledge about its directly accessible reasoning systems, and also about urls to other ONE- brokers on the internet. For example, in our experiments we gained access to the computer algebra system running in Saarbrücken simply by informing our local broker (which for license reasons cannot locally offer a service) about the existence and url of the Saarbrücken broker. The Saarbrücken broker then connects our local broker indirectly with the service. Currently our system links up with the computer algebra systems and running in Saarbrücken, and locally with the higher-order theorem provers and , the first-order theorem prover (employed also as our propositional logic specialist), and (employed as a model generator).

Once the reactive suggestion mechanism dynamically updates and heuristically sorts the list of suggestions, which are commands together with their particular parameter instantiations, it passes the list on to the selector. Its main task is to automatically execute the heuristically preferred command, and hence, initiate an update of the proof data structure. Furthermore, the selector stores the non-optimal, alternative command suggestions in a special store. The information in this store is used when backtracking to a previous state in the proof data structure becomes necessary. Instead of a complete initialisation the reactive suggestion mechanism is then simply initialised with the already computed backtracking information for the current proof context. Backtracking is caused when the reactive layer produces no suggestions or when a user defined maximal depth in the proof data structure is reached.

The backtrack store maintains backtracking information for the proof data structure. This information includes representations of the suggestion computations that have been previously computed but not executed. Additionally the store maintains the results of external system calls modulo their translation in the core natural deduction calculus. That is, the immediate translation of external system results is also done by the reactive suggestion layer, and the results of these computations are memorised for backtracking purposes as well. If the system or the user selects to apply the result of an external system, the proof data structure is updated with the translated proof object. Future work will include investigating whether the backtrack store should be merged with the proof data structure. The idea is that each single node in a proof directly maintains its backtracking alternatives instead of using an indirect maintenance via the backtracking store.

The tasks of the user interface in our framework are:

1.

To visualise the current proof data structure and to ease interactive proof construction. For this purpose we employ 's graphical user interface  [Siekmann et al.1999].

2.

To dynamically present to the user the set of suggestions, which pop up from the reactive layer to the user and to provide support for analysing or executing them. This is realised by structured and dynamically updated pop-up windows in .

3.

To provide graphical support for analysing the results of external systems, that is, to display their results after translation/representation in the proof data structure. We achieve this by extending so that it can switch between the global proof data structure and locally offered results by external systems.

4.

To support the user in interacting with the automated mechanism and in customising agent societies at run-time.

From an abstract perspective, our system realises proof construction by going through a cycle which consists of assessing the state of the proof search process, evaluating the progress, choosing a promising direction for further search and redistributing the available resources accordingly. If the current search direction becomes increasingly less promising then backtracking to previous points in the search space is possible. Only successful or promising proof attempts are allowed to continue searching for a proof. This process is repeated until a proof is found, or some other terminating condition is reached.

  
Experiments

In this subsection we report on experiments we conducted with our system to demonstrate the usefulness of a flexible combination of different specialised reasoning systems. Among others we examined three different problem classes:

1.

  Set examples which demonstrate a cooperation between higher-order and first-order theorem provers. For instance:
$\forall x,y,z \lambdot (x = y \cup z) \Leftrightarrow$
$(y \subseteq x \wedge z \subseteq x \wedge \forall v \lambdot (y \subseteq v \wedge z \subseteq v) \Rightarrow (x \subseteq v)$

2.

  Set equations whose validity/invalidity is decided in an interplay of a natural deduction calculus with a propositional logic theorem prover and model generator. For instance:

(a)

  $\forall x,y,z \lambdot (x \cup y) \cap z = (x \cap z) \cup (y \cap z)$

(b)

  $\forall x,y,z \lambdot (x \cup y) \cap z = (x \cup z) \cap (y \cup z)$

3.

  Concrete examples about sets over naturals where a cooperation with a computer algebra system is required. For instance (gcd and lcm stand for the `greatest common divisor' and the `least common multiple'):

$\{x \vert x > gcd(10,8) \wedge x < lcm(10,8)\} =$
$\{x \vert x < 40\} \cap \{x \vert x > 2\}$

This set is represented by the lambda expression

$(\lambda x \sdot x > gcd(10,8) \wedge x < lcm(10,8)) =$
$(\lambda x \sdot x < 40) \cap (\lambda x \sdot x > 2)$

We will sketch in the following how the problem classes are solved in our system in general and how the proofs of the concrete examples work in particular.

(1).

The first type of examples is motivated by the shortcomings of existing higher-order theorem provers in first-order reasoning. For our experiments we used the system [Benzmüller and Kohlhase1998], a higher-order resolution prover, which specialises in extensionality reasoning and is particularly successful in reasoning about sets.

  

Figure 2: Agent based cooperation between Leo and Otter.

Initialised with a set problem tries to apply extensionality reasoning in a goal directed way. On an initial set of higher-order clauses, it often quickly derives a corresponding set of essentially first-order clauses. Depending on the number of generated first-order and other higher-order clauses may practically get stuck in its reasoning process, although the subset of first-order clauses could be easily refuted by a first-order specialist.

For our examples the cooperation between and a first-order specialist works as depicted in Figure 2. Part 1 of Figure 2 describes the initial problem representation in the proof data structure. The initialisation triggers the agents of the reactive suggestion layer which now start their computations in order to produce suggestions for the next proof step.

The agent working for first checks if there is any information from the resource agent that indicates that should stay passive. If not, it checks whether the goal C is suitable for by testing if it is a higher-order problem. In case the problem is higher-order the agent passes the initial problem consisting of the goal C and the assumptions P₁,...P_n. to Leo. While working on the input problem (as indicated by the shaded oval in Part 2 of Figure 2) derives (among others) various essentially first-order clauses (e.g.  FO₁,...,FO_n). Notice that after a while this subset becomes large enough to be independently refutable. If after consuming all the resources made available by the reactive suggestion layer still fails to deliver a completed proof, it then offers a partial proof consisting of a subset of first-order and essentially first-order clauses (after translation into prenex normal form, e.g.  $\forall \overline{x} \lambdot \mbox{FO}'_1 \wedge \ldots \wedge \mbox{FO}'_n$, where the FO_i^' are disjunctions of the literals of FO_i and $\overline{x}$ stands for the sequence of all free variables in the scope). In case 's suggestion wins over the suggestions computed by other agents, then its partial result is represented in the proof data structure and the reactive suggestion mechanism is immediately triggered again to compute a suggestion for the next possible proof step. Since Leo's partial result is now the new subgoal of the partial proof, first-order agents like the one working for can pick it up and ask to prove it (see Part 3 of Figure 2). If signals a successful proof attempt before consuming all its given resources, its resolution proof is passed to the natural deduction translation module [Meier2000], which transforms it into a proper natural deduction proof on an assertion level.

We experimented with 121 simple examples, that is, examples that can be automatically proved by alone. The results showed that the command execution interval chosen by the selector is crucial, since it determines the computation time ct made available to the external systems.

• If ct is sufficiently high, then the problem is automatically proved by (for the simple examples tested here).
• If ct is not sufficient for to come up with a proof, but still enough to produce a refutable subset of essentially first-order clauses, then a cooperative proof is constructed as described above.
• If ct is not sufficient to even guarantee a subset of refutable essentially first-order clauses, then the problem is tackled purely on natural deduction level, however not necessarily successful.

We also solved 5 examples, which cannot be solved with alone. One of them is the concrete example given above, which, to our knowledge cannot be solved by a single automated theorem prover. In our experiments, ran out of memory for the above problem formulation and could not find a proof after running 24 hours in auto mode on a first-order formulation of the problem.

(2).

The second type of set examples illustrates a cooperation between automated natural deduction agents, a propositional prover, and a model generator. The proofs follow a well-known set theoretic proof principle: they are constructed first by application of simple natural deduction agents that reduce the set equations by applying set extensionality and definition expansion to a propositional logic statement. This statement is then picked up by an agent working for a propositional logic prover (here we use again encapsulated in another agent shell with a slightly modified applicability check and a different representation translation approach) and a counter-example agent which employs . The logic statement is then either proved or refuted. Thus, valid and invalid statements are tackled analogously in all but the last step.

In case (2a) of our concrete examples several $\forall_I$(universal quantification introduction in backward reasoning) applications introduce $(a \cup b) \cap c = (a \cap c) \cup (b \cap c)$ as new open subgoal. Set extensionality gives us $\forall u \lambdot u \in (a \cup b) \cap c \Leftrightarrow u \in ((a \cap c) \cup (b \cap c))$. A further $\forall_I$ application and subsequent definition expansions (where $a \cup b := \lambda z \lambdot (z \in a) \vee (z \in b)$, $a \cap b := \lambda z \lambdot (z \in a) \wedge (z \in b)$, and $u \in a:= a(u)$) reduce this goal finally to $(a(d) \vee b(d)) \wedge c(d) = (a(d) \wedge c(d)) \vee (b(d) \wedge c(d))$ which contains no variables and which is a trivial task for any propositional logic prover. In case (2b) we analogously derive $(a(d) \vee b(d)) \wedge c(d) = (a(d) \vee c(d)) \wedge (b(d) \vee c(d))$, but instead of employing the propositional prover, the system now uses a model generator which presents the counter-model $a(d), b(d), \neg c(d)$, that is, it points to the set of all d such that $d\in a$, $d\in b$, but $d\notin c$. Hence, the model generator came up with a counter-example to the expression in (2b). Future work includes integrating facilities for the visualisation of these counter-examples by Venn diagrams in .

We have experimented with an automatically and systematically generated testbed of 20363 examples consisting of all possible set equations involving $\cap,\cup, set-minus$ operations up to nesting depth of 5 in maximally 5 variables. So far we classified the first 10000 of these examples with our system discovering 988 correct and 9012 false statements. Naturally, the correct statements are probably also solvable with the cooperation of and .

(3).

The next type of examples has cross-domain character and requires a combination of domain specific systems. In order to tackle them we added a simplification agent which links the computer algebra system to our core system. As an application condition this agent checks whether the current subgoal contains certain simplifiable expressions. If so, then it simplifies the subgoal by sending the simplifiable subterms (e.g.  x > gcd(10,8)) via to and replaces them with the corresponding simplified terms (e.g. x > 40). Hence, the new subgoal suggested by the simplification agent is: $(\lambda x \sdot x > 2 \wedge x < 40) = (\lambda x \sdot x < 40) \cap (\lambda x \sdot x > 2)$. Since no other agent comes up with a better alternative, this suggestion is immediately selected and executed. Subsequently the agent successfully attacks the new goal after expanding the definition of $\cap$. We have successfully solved 12problems of the given type and intend to generate a large testbed next.

.

Our experiments show that the cooperation between different kinds of reasoning systems can fruitfully combine their different strengths and even out their respective weaknesses. In particular, we were able to successfully employ 's extensionality reasoning with 's strength in refuting large sets of first-order clauses. Thus, we were able to tackle problems previously unsolved by a single system. Likewise, our distributed architecture enables us to exploit the computational strength of in our examples remotely over the internet.

Note that our approach does not only allow the combination of heterogeneous systems to prove a problem, but it also enables the use of systems with opposing goals in the same framework. In our examples the theorem prover and the model generator work in parallel to decide the validity of the current goal. More importantly, further reasoning systems - in form of reasoning agents - can easily be integrated (this is true in particular for systems which have an interface to the system). The system we developed is the most comprehensive and general approach to integrating heterogeneous reasoning systems for automated and interactive theorem proving.

As we knew when we started the project (and this was appreciated by the reviewers), not all problems in this area can be finally solved in a one year project. The experience of the project points to different lines of future research. Firstly, the agent approach offers an interesting framework for combining automated and interactive theorem proving. In order to do this adequately, a more distributed view of proof construction and a dynamic configuration of cooperating agents seems to be necessary. Secondly, in order to concurrently follow different lines of search, a more sophisticated resource handling should be added to the system. Thirdly the communication overhead for obtaining large proofs is the main performance bottleneck. More efficient communication facilities between the different systems involved have to be developed.

Project Plan Review

The project plan proved to be feasible and has been carried through as in the application.

Research Impact and Benefits to Society

In this project we intensively tested the system. The methodology developed has a great potential for being applied in the combination of different reasoning system in a flexible way, which does not require hard-wiring. Some experimental results of our project (the automated solution of non-trivial problems from set theory) are an important precondition to research projects at the University of Saarbrücken (DIALOG project on Natural Language Tutorial Dialogue to a Mathematical Assistance System and $\lambda$-PLAN). We discussed with Prof Michael Fisher, Liverpool, applications of the methodology in temporal distributed theorem proving.

In this project we closely collaborated with Volker Sorge and other members of the group in Saarbrücken. This collaboration resulted in joint publications. We received support from the developers, Jürgen Zimmer (Genova) and Andreas Franke (Saarbrücken).

We plan to continue and deepen cooperation with the University of Saarbrücken in this project, where the former research fellow took up the post of the leader of the group.

   
Further Research or Dissemination Activities

We have dissiminated the results by presenting our work to other researchers through formal presentations at conferences, informal research visits and publications accounting this research. In particular Christoph Benzmüller has given presentations at the Universities of Birmingham, Edinburgh, Manchester Metropolitan University, York. He also presented the work in an invited talk at AISB-2001/AR-2001 (Annual Meeting of the Society for Artificial Intelligence and Simulated Behaviour, and the Automated Reasoning Workshop) in York. The system developed in the project has been installed and presented at the University of Edinburgh during a two month research visit of Dr Benzmüller.

We plan an ongoing cooperation on this issue with the University of Saarbrücken, in person of Dr Christoph Benzmüller, now head of the group, and the other group member. We plan to exploit the positive results of this project in another project we will apply for in the near future, jointly with Prof Fisher, University of Liverpool and would like to employ Volker Sorge as research fellow.

In addition to the publications [Benzmüller and Sorge2000,Benzmüller et al.2000,Benzmüller2001] available already, one conference contribution [Benzmüller and Kerber2001] is currently submitted and a second [Benzmüller et al.2000] will be submitted shortly. Furthermore, a journal publication is in preparation [Benzmüller et al.2000]. All results will be documented on the web page of the project at http://www.cs.bham.ac.uk/ mmk/projects/AOTP/index.html.

Bibliography

Armando and Zini2000

A. Armando and D. Zini. Interfacing Computer Algebra and Deduction Systems via the Logic Broker Architecture. In Proc. of the 8th Calculemus Symposium, 2000. A.K.Peters.

Benzmüller and Kohlhase1998

C. Benzmüller and M. Kohlhase.
LEO -- a higher order theorem prover.
of CADE-15, 1421, 1998. Springer.

Benzmüller and Sorge2000

C. Benzmüller and V. Sorge.
OANTS -- an open approach at combining interactive and automated theorem proving.
In Proc. of the 8th Calculemus Symposium, 2000. A.K.Peters.

Benzmüller et al.2000

C. Benzmüller, M. Jamnik, M. Kerber, and V. Sorge.
Resource guided concurrent deduction.
In Proc. of the 8th Calculemus Symposium, 2000. A.K.Peters. (Also in Proceedings of the AISB'2000 Symposium `How to design a functioning mind', Birmingham, England, April 2000 and Proceedings of the 7th Workshop on Automated Reasoning `Bridging the Gap between Theory and Practice'.)

Benzmüller2001

C. Benzmüller.
An agent based approach to reasoning.
Extended abstract for invited plenary talk at AISB'01 Convention `Agents and Cognition, University of York, England, March 2001.

Benzmüller and Kerber2001

C. Benzmüller and M. Kerber.
A Lost Proof.
submitted.

Benzmüller et al.2000

C. Benzmüller, M. Jamnik, M. Kerber, and V. Sorge.
An agent-oriented approach to reasoning.
submitted shortly.

Benzmüller et al.2000

C. Benzmüller, M. Jamnik, M. Kerber, and V. Sorge.
Towards concurrent resource managed deduction.
in preparation.

Denzinger and Fuchs1999

J. Denzinger and D. Fuchs.
Cooperation of Heterogeneous Provers.
of the 16th IJCAI, 1999. Morgan Kaufmann.

Denzinger et al.1997

J. Denzinger, J. Kronenburg, and S. Schulz.
DISCOUNT - A Distributed and Learning Equational Prover.
, 18(2):189-198, 1997.

Fisher and Ireland1998

M. Fisher and A. Ireland.
Multi-agent proof-planning.
Workshop ``Using AI methods in Deduction'', CADE-15, 1998.

Fisher1997

M. Fisher.
An Open Approach to Concurrent Theorem Proving.
Parallel Processing for Artificial Intelligence, volume 3. Elsevier/North Holland, 1997.

Franke et al.1999

A. Franke, S. Hess, Ch. Jung, M. Kohlhase, and V. Sorge.
Agent-Oriented Integration of Distributed Mathematical Services.
Journal of Universal Computer Science, 5(3):156-187, 1999.

Meier2000

Andreas Meier.
TRAMP -- Transformation of machine-found proofs into ND-proofs at the assertion level.
of CADE-17, 1831, 2000. Springer.

Omega Group1997

The Omega Group.
$\Omega$MEGA: Towards a mathematical assistant.
of CADE-14, 1249, 1997. Springer.

Siekmann et al.1999

J. Siekmann, et al.
$\cal LOUI$: $\cal L$ovely $\cal U$ser $\cal I$nterface.
Formal Aspects of Computing, 11(3):326-342, 1999.

Wolf1998

A. Wolf.
P-SETHEO: Strategy Parallelism in Automated Theorem Proving.
Proc. of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 1397, 1998. Springer.

About this document ...

Agent-Oriented Theorem Proving

EPSRC Grant: GR/M99644/01 - Review Report

This document was adapted from a file generated by the LaTeX2HTML translator Version 98.1p1 release (March 2nd, 1998)

Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, Computer Based Learning Unit, University of Leeds.

The command line arguments were:
latex2html -split 0 index.tex.

The translation was initiated by Manfred Kerber on 2001-03-29

Footnotes

... CASC

CADE ATP System Competitions, see also http://www.cs.jcu.edu.au/ tptp/.

... depth

Iterative deepening proof search wrt. to the maximal depth is conceptually feasible but not realised yet.

... clauses.

By essentially first-order we mean a clause set that can be tackled by first-order methods. It may still contain higher-order variables, though.

... level.

While already supports the transformation of various machine oriented first-order proof formats, further work will include its extension to higher-order logic, such that also the proof step justified in Figure 2 with `LEO-derivation' can be properly expanded into a verifiable natural deduction proof.