The Experts below are selected from a list of 231 Experts worldwide ranked by ideXlab platform

Peter Baumgartner - One of the best experts on this subject based on the ideXlab platform.

  • Tool Support for System Specification, Development and Verification - Model Elimination with Simplification and its Application to Software Verification
    Tool Support for System Specification Development and Verification, 1999
    Co-Authors: Peter Baumgartner, Dorothea Schäfer
    Abstract:

    Software verification is known to be a notoriously difficult application area for automated theorem provers. Consequently, this is the domain of interactive systems, such as KIV [Reif et al., 1997], HOL [Gordon and Melham, 1993], Isabelle [Nipkow and Paulson, 1992] and PVS [Owre et al., 1992]. The work described here aims to demonstrate that automated theorem provers (ATPs) can be successfully incorporated into such systems in order to relieve the user from some interactions. More specifically, we describe our approach of coupling the interactive program verification system KIV [Reif et al , 1997] with our automated theorem prover PROTEIN [Baumgartner and Furbach, 1994].

  • 3. Tableau Model Elimination
    Theory Reasoning in Connection Calculi, 1998
    Co-Authors: Peter Baumgartner
    Abstract:

    Model Elimination [Loveland, 1968] is a calculus, which is the base of numerous proof procedures for first order deduction. There are high speed theorem provers, like METEOR [Astrachan and Stickel, 1992] or SETHEO [Letz et al., 1992]. The implementation of Model Elimination provers can take advantage of techniques developed for Prolog. For instance, SETHEO compiles the input clause set into a generalized WAM architecture. Stickel’s Prolog technology theorem proving system (PTTP, [Stickel, 1988]) uses Horn clauses as an intermediate language, which can even be processed by conventional Prolog systems [Stickel, 1989].

  • Theory Reasoning in Connection Calculi
    1998
    Co-Authors: Peter Baumgartner
    Abstract:

    In this chapter general theory reasoning versions of a connection calculus (CC) and Model Elimination (ME) will be introduced and gradually refined. Here, the term “general” means that no special properties of a particular theory is made use of. Instead, rather high-level principles for the interaction between the foreground and the background calculi are employed.

  • A Disjunctive Positive Refinement of Model Elimination and its Application to Subsumption Deletion
    Journal of Automated Reasoning, 1997
    Co-Authors: Peter Baumgartner, Stefan Brüning
    Abstract:

    The Model Elimination (ME) calculus is a refutationally complete,goal-oriented calculus for first-order clause logic. In this article, weintroduce a new variant called disjunctive positive ME (DPME); it improveson Plaisted’s positive refinement of ME in that reduction steps areallowed only with positive literals stemming from clauses having at leasttwo positive literals (so-called disjunctive clauses). DPME is motivated byits application to various kinds of subsumption deletion: in order to applysubsumption deletion in ME equally successful as in resolution, it iscrucial to employ a version of ME that minimizes ancestor context (i.e., thenecessary A-literals to find a refutation). DPME meets this demand. Wedescribe several variants of ME with subsumption, the most important onesbeing ME with backward and forward subsumption and theT*-Context Check. We compare their pruning power, also takinginto consideration the well-known regularity restriction. All proofs aresupplied. The practicability of our approach is demonstrated with experiments.

  • Computing answers with Model Elimination
    Artificial Intelligence, 1997
    Co-Authors: Peter Baumgartner, Ulrich Furbach, Frieder Stolzenburg
    Abstract:

    AbstractWe demonstrate that theorem provers using Model Elimination (ME) can be used as answer-complete interpreters for disjunctive logic programming. More specifically, we introduce a family of restart variants of Model Elimination and we introduce a mechanism for computing answers. Building on this, we develop a new calculus called ancestry restart ME. 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 nontrivial answers to goals than to prove the existence of answers

Mark E Stickel - One of the best experts on this subject based on the ideXlab platform.

  • Upside-down meta-interpretation of the Model Elimination theorem-proving procedure for deduction and abduction
    Journal of Automated Reasoning, 1994
    Co-Authors: Mark E Stickel
    Abstract:

    Typical bottom-up, forward-chaining reasoning systems such as hyperresolution lack goaldirectedness, while typical top-down, backward-chaining reasoning systems like Prolog or Model Elimination repeatedly solve the same goals. Reasoning systems that are goal-directed and avoid repeatedly solving the same goals can be constructed by formulating the top-down methods meta-theoretically for execution by a bottom-up reasoning system (hence, we use the term upside-down meta-interpretation). This formulation also facilitates the use of flexible search strategies, such as merit-ordered search, that are common to bottom-up reasoning systems. The Model Elimination theorem-proving procedure, its extension by an assumption rule for abduction, and its restriction to Horn clauses are adapted here for such upside-down meta-interpretation. This work can be regarded as an extension of the magic-sets or Alexander method for query evaluation in deductive databases to both non-Horn clauses and abductive reasoning.

  • CADE - Caching and Lemmaizing in Model Elimination Theorem Provers
    Automated Deduction—CADE-11, 1992
    Co-Authors: Owen Astrachan, Mark E Stickel
    Abstract:

    Theorem provers based on Model Elimination have exhibited extremely high inference rates but have lacked a redundancy control mechanism such as subsumption. In this paper we report on work done to modify a Model Elimination theorem prover using two techniques, caching and lemmaizing, that have reduced by more than an order of magnitude the time required to find proofs of several problems and that have enabled the prover to prove theorems previously unobtainable by top-down Model Elimination theorem provers.

  • caching and lemmaizing in Model Elimination theorem provers
    Conference on Automated Deduction, 1992
    Co-Authors: Owen Astrachan, Mark E Stickel
    Abstract:

    Theorem provers based on Model Elimination have exhibited extremely high inference rates but have lacked a redundancy control mechanism such as subsumption. In this paper we report on work done to modify a Model Elimination theorem prover using two techniques, caching and lemmaizing, that have reduced by more than an order of magnitude the time required to find proofs of several problems and that have enabled the prover to prove theorems previously unobtainable by top-down Model Elimination theorem provers.

  • CADE - A Prolog Technology Theorem Prover
    10th International Conference on Automated Deduction, 1990
    Co-Authors: Mark E Stickel
    Abstract:

    An extension of Prolog, based on the Model Elimination theorem-proving procedure, would permit production of a logically complete Prolog technology theorem prover capable of performing inference operations at a rate approaching that of Prolog itself.

Paul R. Gooley - One of the best experts on this subject based on the ideXlab platform.

  • Model-free Model Elimination: A new step in the Model-free dynamic analysis of NMR relaxation data
    Journal of Biomolecular NMR, 2006
    Co-Authors: Edward J. D’auvergne, Paul R. Gooley
    Abstract:

    Model-free analysis is a technique commonly used within the field of NMR spectroscopy to extract atomic resolution, interpretable dynamic information on multiple timescales from the R _1, R _2, and steady state NOE. Model-free approaches employ two disparate areas of data analysis, the discipline of mathematical optimisation, specifically the minimisation of a χ^2 function, and the statistical field of Model selection. By searching through a large number of Model-free minimisations, which were setup using synthetic relaxation data whereby the true underlying dynamics is known, certain Model-free Models have been identified to, at times, fail. This has been characterised as either the internal correlation times, τ_ e , τ_ f , or τ_ s , or the global correlation time parameter, local τ_ m , heading towards infinity, the result being that the final parameter values are far from the true values. In a number of cases the minimised χ^2 value of the failed Model is significantly lower than that of all other Models and, hence, will be the Model which is chosen by Model selection techniques. If these Models are not removed prior to Model selection the final Model-free results could be far from the truth. By implementing a series of empirical rules involving inequalities these Models can be specifically isolated and removed. Model-free analysis should therefore consist of three distinct steps: Model-free minimisation, Model-free Model Elimination, and finally Model-free Model selection. Failure has also been identified to affect the individual Monte Carlo simulations used within error analysis. Each simulation involves an independent randomised relaxation data set and Model-free minimisation, thus simulations suffer from exactly the same types of failure as Model-free Models. Therefore, to prevent these outliers from causing a significant overestimation of the errors the failed Monte Carlo simulations need to be culled prior to calculating the parameter standard deviations.

Ulrich Furbach - One of the best experts on this subject based on the ideXlab platform.

  • Computing answers with Model Elimination
    Artificial Intelligence, 1997
    Co-Authors: Peter Baumgartner, Ulrich Furbach, Frieder Stolzenburg
    Abstract:

    AbstractWe demonstrate that theorem provers using Model Elimination (ME) can be used as answer-complete interpreters for disjunctive logic programming. More specifically, we introduce a family of restart variants of Model Elimination and we introduce a mechanism for computing answers. Building on this, we develop a new calculus called ancestry restart ME. 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 nontrivial answers to goals than to prove the existence of answers

  • IJCAI - Model Elimination, logic programming and computing answers
    1995
    Co-Authors: Peter Baumgartner, Ulrich Furbach, Frieder Stolzenburg
    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 ME. 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.

  • Model Elimination without contrapositives and its application to PTTP
    Journal of Automated Reasoning, 1994
    Co-Authors: Peter Baumgartner, Ulrich Furbach
    Abstract:

    We give modifications of Model Elimination that 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. We relate our results to other calculi, namely, the connection method, modified problem reduction format, and near-Horn Prolog.

  • CADE - Model Elimination Without Contrapositives
    Automated Deduction — CADE-12, 1994
    Co-Authors: Peter Baumgartner, Ulrich Furbach
    Abstract:

    We present modifications of Model Elimination which do not necessitate the use of contrapositives. These restart Model Elimination calculi are proven sound and complete. 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.

  • CADE - PROTEIN: A PROver with a Theory Extension INterface
    Automated Deduction — CADE-12, 1994
    Co-Authors: Peter Baumgartner, Ulrich Furbach
    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.

Owen Astrachan - One of the best experts on this subject based on the ideXlab platform.

  • METEOR: Exploring Model Elimination theorem proving
    Journal of Automated Reasoning, 1994
    Co-Authors: Owen Astrachan
    Abstract:

    In this paper we describe the theorem prover METEOR which is a high-performance Model Elimination prover running in sequential, parallel, and distributed computing environments. METEOR has a very high inference rate. But, as is the case with better chess-playing programs, speed alone is not sufficient when exploring large search spaces; intelligent search is necessary. We describe modifications to traditional iterative deepening search mechanisms whose implementation in METEOR result in performance improvements of several orders of magnitude and that have permitted the discovery of proofs unobtainable by top-down Model Elimination provers.

  • CADE - Caching and Lemmaizing in Model Elimination Theorem Provers
    Automated Deduction—CADE-11, 1992
    Co-Authors: Owen Astrachan, Mark E Stickel
    Abstract:

    Theorem provers based on Model Elimination have exhibited extremely high inference rates but have lacked a redundancy control mechanism such as subsumption. In this paper we report on work done to modify a Model Elimination theorem prover using two techniques, caching and lemmaizing, that have reduced by more than an order of magnitude the time required to find proofs of several problems and that have enabled the prover to prove theorems previously unobtainable by top-down Model Elimination theorem provers.

  • caching and lemmaizing in Model Elimination theorem provers
    Conference on Automated Deduction, 1992
    Co-Authors: Owen Astrachan, Mark E Stickel
    Abstract:

    Theorem provers based on Model Elimination have exhibited extremely high inference rates but have lacked a redundancy control mechanism such as subsumption. In this paper we report on work done to modify a Model Elimination theorem prover using two techniques, caching and lemmaizing, that have reduced by more than an order of magnitude the time required to find proofs of several problems and that have enabled the prover to prove theorems previously unobtainable by top-down Model Elimination theorem provers.

  • Dagstuhl Seminar on Parallelization in Inference Systems - METEORs: High Performance Theorem Provers Using Model Elimination
    Automated Reasoning Series, 1990
    Co-Authors: Owen Astrachan
    Abstract:

    \indent Historically, depth-first (linear) resolution procedures have not fared well in proving deeper theorems relative to breadth-first resolution provers of various types, primarily because of the search redundancy problem. However, we can now demonstrate that the Model Eliminator (ME) procedure, a linear-input resolution-like procedure, may be a superior approach for certain types of problems (generally non-Horn problems). There is a conjunction of reasons why the METEOR provers presently appear so effective. The reasons are: the inherent speed advantage of linear input systems, the sophistication of the WAM architecture in exploiting this advantage, a program written in the language C using tight coding and effective data structures, the speed of the platforms on which they run, and the successful use of different search strategies. We explore single processor and parallel processor implementations of ME using different versions of interactive depth-first search. Among the theorems we prove are variants of a problem in calculus for which this ME theorem prover is presently the only uniform first-order proof procedure realization that has succeeded in proving these variants.