1 - 7 of 7 articles
In this paper we describe the theorem proverMETEOR 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...
In this paper techniques are developed and compared that increase the inferential power of tableau systems for classical first-order logic. The mechanisms are formulated in the framework of connection tableaux, which is an amalgamation of the connection method and the tableau calculus, and a...
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,...
In this paper a refutation calculus for intuitionistic predicate logic is presented where the necessity of duplicating formulas to which rules are applied is analyzed. In line with the semantics of intuitionistic logic in terms of Kripke models a new signF
beside the SignsT andF is added which...
We present a tableau-based proof procedure forvariable domain-minimal entailment, a nonmonotonic entailment relation closely related to McCarthy's domain circumscription. By using a modified tableau rule for existential formulas, an idea first suggested by Hintikka, we construct partial and in a...
A new type of tableau system is proposed for the complete class (called miniscoped Horn-like) of first-order linear temporal logic. The described system instead of induction-like postulates contains some nonlogical axioms indicating the saturation of a derivation process in this system.
A list of tableau-based theorem provers was assembled in spring and summer 1993 as the result of a widespread enquiry via e-mail. It is intended to provide a brief overview of the field and existing implementations. For each system, a short description is given. Additionally, useful information...
Read and print from thousands of top scholarly journals.
Continue with Facebook
Log in with Microsoft
Already have an account? Log in
Bookmark this article. You can see your Bookmarks on your DeepDyve Library.
To save an article, log in first, or sign up for a DeepDyve account if you don’t already have one.
Sign Up Log In
To subscribe to email alerts, please log in first, or sign up for a DeepDyve account if you don’t already have one.
To get new article updates from a journal on your personalized homepage, please log in first, or sign up for a DeepDyve account if you don’t already have one.