|
|
Close Help | ||||||||||||||
|
|
|
Close Help | ||||||||||||||
The PROTEIN system description. Should give you an overview of the system. Click here to get the report.
Abstract: PROTEIN (PROver with a Theory Extension INterface) is a PTTP-based first order theorem prover over built-in theories. Besides various standard-refinements known for model elimination, PROTEIN also offers a variant of model elimination for case-based reasoning and which does not need contrapositives.
This is the primary text for ``restart model elimination'', one of the calculus variants featured in PROTEIN. Click here to get the report.
Abstract: We give modifications of model elimination which do not necessitate the use of contrapositives. These restart model elimination calculi are proven sound and complete and their implementation by PTTP is depicted. The corresponding proof procedures are evaluated by a number of runtime experiments and they are compared to other well known provers. Finally we relate our results to other calculi, namely the connection method, modified problem reduction format and Near-Horn Prolog.
This paper introduces the ancestry variant of restart model elimination; it is the preferred version for computing minimal answers. Click here to get the report.
Abstract: We demonstrate that theorem provers using model elimination (ME) can be used as answer-complete interpreters for disjunctive logic programming. More specifically, we introduce a mechanism for computing answers into the restart variant of ME. Building on this we develop a new calculus called ancestry restart. This variant admits a more restrictive regularity restriction than restart ME, and, as a side effect, it is in particular attractive for computing definite answers. The presented calculi can also be used successfully in the context of automated theorem proving. We demonstrate experimentally that it is more difficult to compute (non-trivial) answers to goals, instead of only proving the existence of answers.
This is the primary text for the theory extensions of model elimination as to be found in PROTEIN. It is the long version including all proofs. Click here to get the report.
Abstract: Theory Reasoning means to build-in certain knowledge about a problem domain into a deduction system or calculus, which is in our case model elimination. Several versions of theory model elimination (TME) calculi are presented and proven complete: on the one hand we have highly restricted versions of total and partial TME. These restrictions allow (1) to keep fewer path literals in extension steps than in related calculi, and (2) discard proof attempts with multiple occurrences of literals along a path (i.e.\ regularity holds). On the other hand, we obtain by small modifications to TME versions which do not need contrapositives (a la Near-Horn Prolog). We show that regularity can be adapted for these versions. The independence of the goal computation rule holds for all variants.
Comparative runtime results for our PTTP-implementations are supplied.
This paper introduces the computation of negation according to WGCWA or GCWA. Click here here to get the report.
Abstract: In this paper, we study an abductive framework for disjunctive logic programming that provides a new way to understand negation in disjunctive logic programming. We show that the defined framework captures the existing minimal model semantics based on (Extended) Generalised Closed World Assumption ((E)GCWA). This relationship between abduction and minimal model reasoning provides a methodology to develop algorithms for minimal model reasoning. To demonstrate this, we show how a theorem prover, based on restart model elimination calculus, can be modified for abductive reasoning and thus for minimal model reasoning.
This text describes the method of linearizing completion in detail. It is the backbone of the LC tool. Click here to get the report.
Abstract: We present a new transformation method by which a given Horn theory is transformed in such a way that resolution derivations can be carried out which are both linear (in the sense of Prologs SLD-resolution) and unit-resulting (i.e. the resolvents are unit clauses). This is not trivial since although both strategies alone are complete, their naive combination is not. Completeness is recovered by our method through a completion procedure in the spirit of Knuth-Bendix completion, however with different ordering criteria. A powerful redundancy criterion helps to find a finite system quite often.
The transformed theory can be used in combination with linear calculi such as e.g.\ (theory) model elimination to yield sound, complete and efficient calculi for full first order clause logic over the given Horn theory.
As an example application, our method discovers a generalization of the well-known linear paramodulation calculus for the combined theory of equality and strict orderings.
The method has been implemented and has been tested in conjunction with a model elimination theorem prover.
This text describes how to bring in simplification into Model Elimination and reports on practical experiments carried out with PROTEIN. Click here to get the report.
Abstract: This work is motivated by a coupling of the interactive software verification system KIV with our Model Elimination prover PROTEIN. In order to make this combination efficient, we extend Model Elimination by a concept of simplification based on conditional rewrite rules. The extension is defined in such a way that rewrite rules as given from the KIV system can easily be accommodated. In the paper, we describe the new simplification technique, discuss completeness, and demonstrate with practical practical experiments from the KIV domain the benefits.
