The Experts below are selected from a list of 35319 Experts worldwide ranked by ideXlab platform
John Slaney - One of the best experts on this subject based on the ideXlab platform.
-
CADE - Scavenger 0.1: A Theorem Prover Based on Conflict Resolution
Automated Deduction – CADE 26, 2017Co-Authors: Daniyar Itegulov, John Slaney, Bruno Woltzenlogel PaleoAbstract:This paper introduces Scavenger, the first Theorem Prover for pure first-order logic without equality based on the new conflict resolution calculus. Conflict resolution has a restricted resolution inference rule that resembles (a first-order generalization of) unit propagation as well as a rule for assuming decision literals and a rule for deriving new clauses by (a first-order generalization of) conflict-driven clause learning.
-
Scavenger 0.1: A Theorem Prover Based on Conflict Resolution
arXiv: Logic in Computer Science, 2017Co-Authors: Daniyar Itegulov, John Slaney, Bruno Woltzenlogel PaleoAbstract:This paper introduces Scavenger, the first Theorem Prover for pure first-order logic without equality based on the new conflict resolution calculus. Conflict resolution has a restricted resolution inference rule that resembles (a first-order generalization of) unit propagation as well as a rule for assuming decision literals and a rule for deriving new clauses by (a first-order generalization of) conflict-driven clause learning.
-
scott a model guided Theorem Prover
International Joint Conference on Artificial Intelligence, 1993Co-Authors: John SlaneyAbstract:SCOTT (Semantically Constrained Otter) is a resolution-based automatic Theorem Prover for first order logic. It is based on the high performance Prover OTTER by W. McCune and also incorporates a model generator. This finds finite models which SCOTT is able to use in a variety of ways to direct its proof search. Clauses generated by the Prover are in turn used as axioms of theories to be modelled. Thus Prover and model generator inform each other dynamically. This paper describes the algorithm and some sample results.
-
CADE - ROO: A Parallel Theorem Prover
Automated Deduction—CADE-11, 1992Co-Authors: Ewing Lusk, William Mccune, John SlaneyAbstract:We describe a parallel Theorem Prover based on the Argonne Theorem-proving system OTTER. The parallel system, called Roo, runs on shared-memory multiprocessors such as the Sequent Symmetry. We explain the parallel algorithm used and give performance results that demonstrate near-linear speedups on large problems.
Nicola Olivetti - One of the best experts on this subject based on the ideXlab platform.
-
TABLEAUX - CSymLean: a Theorem Prover for the logic CSL over symmetric minspaces
Lecture Notes in Computer Science, 2011Co-Authors: Regis Alenda, Nicola OlivettiAbstract:The logic CSL of comparative concept similarity has been introduced by Sheremet, et al. to capture a form of qualitative similarity comparison. We present here CSymLean, the first Theorem-Prover for CSL interpreted on symmetric minspaces. It is a Prolog implementation of a labelled tableau calculus recently proposed for this logic, and it is inspired by the Lean methodology.
-
A sequent calculus and a Theorem Prover for standard conditional logics
ACM Transactions on Computational Logic, 2007Co-Authors: Nicola Olivetti, Gian Luca Pozzato, Camilla SchwindAbstract:In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity bounds for the respective logics. We also show that these calculi can be the base for uniform proof systems. Moreover, we present CondLean, a Theorem Prover in Prolog for these calculi.
-
A Sequent Calculus and a Theorem Prover for Standard Conditional Logics
arXiv: Logic in Computer Science, 2004Co-Authors: Nicola Olivetti, Gian Luca Pozzato, Camilla SchwindAbstract:In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics, namely CK, CK+ID, CK+MP and CK+MP+ID. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity bounds for the respective logics. We also present CondLean, a Theorem Prover for these logics implementing SeqS calculi written in SICStus Prolog.
Gernot Stenz - One of the best experts on this subject based on the ideXlab platform.
-
dctp a disconnection calculus Theorem Prover system abstract
International Joint Conference on Automated Reasoning, 2001Co-Authors: Reinhold Letz, Gernot StenzAbstract:We describe the Theorem Prover DCTP, which is an implementation of the disconnection tableau calculus, a confluent tableau method, in which free variables are treated in a non-rigid manner. In contrast to most other free-variable tableau variants, the system can also be used for model generation. We sketch the underlying calculus and its refinements, and present the results of an experimental evaluation.
-
IJCAR - DCTP - A Disconnection Calculus Theorem Prover - System Abstract
Automated Reasoning, 2001Co-Authors: Reinhold Letz, Gernot StenzAbstract:We describe the Theorem Prover DCTP, which is an implementation of the disconnection tableau calculus, a confluent tableau method, in which free variables are treated in a non-rigid manner. In contrast to most other free-variable tableau variants, the system can also be used for model generation. We sketch the underlying calculus and its refinements, and present the results of an experimental evaluation.
-
e setheo an automated3 Theorem Prover
Theorem Proving with Analytic Tableaux and Related Methods, 2000Co-Authors: Gernot Stenz, Andreas WolfAbstract:We have developed a method for strategy evaluation and selection based on test data generated from the problem domain. We present the Theorem Prover e-SETHEO, which automatically handles training data management, strategy evaluation and selection, and actual proof tasks. We also give some experimental data produced with this system. We address the problem of test set extraction and give an assessment of our work.
Gian Luca Pozzato - One of the best experts on this subject based on the ideXlab platform.
-
TABLEAUX - KLMLean 2.0: A Theorem Prover for KLM Logics of Nonmonotonic Reasoning
Lecture Notes in Computer Science, 2007Co-Authors: Laura Giordano, Valentina Gliozzi, Gian Luca PozzatoAbstract:We present KLMLean 2.0, a Theorem Prover for propositional KLM logics of nonmonotonic reasoning. KLMLean 2.0 implements some analytic tableaux calculi for these logics recently introduced. KLMLean 2.0 is inspired by the "lean" methodology, it is implemented in SICStus Prolog and it also contains a graphical interface written in Java.
-
A sequent calculus and a Theorem Prover for standard conditional logics
ACM Transactions on Computational Logic, 2007Co-Authors: Nicola Olivetti, Gian Luca Pozzato, Camilla SchwindAbstract:In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity bounds for the respective logics. We also show that these calculi can be the base for uniform proof systems. Moreover, we present CondLean, a Theorem Prover in Prolog for these calculi.
-
A Sequent Calculus and a Theorem Prover for Standard Conditional Logics
arXiv: Logic in Computer Science, 2004Co-Authors: Nicola Olivetti, Gian Luca Pozzato, Camilla SchwindAbstract:In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics, namely CK, CK+ID, CK+MP and CK+MP+ID. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity bounds for the respective logics. We also present CondLean, a Theorem Prover for these logics implementing SeqS calculi written in SICStus Prolog.
Reinhold Letz - One of the best experts on this subject based on the ideXlab platform.
-
dctp a disconnection calculus Theorem Prover system abstract
International Joint Conference on Automated Reasoning, 2001Co-Authors: Reinhold Letz, Gernot StenzAbstract:We describe the Theorem Prover DCTP, which is an implementation of the disconnection tableau calculus, a confluent tableau method, in which free variables are treated in a non-rigid manner. In contrast to most other free-variable tableau variants, the system can also be used for model generation. We sketch the underlying calculus and its refinements, and present the results of an experimental evaluation.
-
IJCAR - DCTP - A Disconnection Calculus Theorem Prover - System Abstract
Automated Reasoning, 2001Co-Authors: Reinhold Letz, Gernot StenzAbstract:We describe the Theorem Prover DCTP, which is an implementation of the disconnection tableau calculus, a confluent tableau method, in which free variables are treated in a non-rigid manner. In contrast to most other free-variable tableau variants, the system can also be used for model generation. We sketch the underlying calculus and its refinements, and present the results of an experimental evaluation.
-
setheo a high performance Theorem Prover
Journal of Automated Reasoning, 1992Co-Authors: Reinhold Letz, Johann Schumann, S. Bayerl, W. BibelAbstract:A sound and complete Theorem Prover for first-order logic is presented, which is based on the connection method. The inference machine is implemented using PROLOG technology, an approach taken also with other systems, most prominently with Stickel's PTTP. But SETHEO differs from those in essential characteristics, among which are the following ones. It incorporates a powerful preprocessing module for a reduction of the input formula. The main proof procedure is realized as a variant of Warren's abstract machine. For search pruning we perform subsumption and regular proofs. Factorization, lemma generation, and the application of proof schemata are offered as options. The entire system is implemented in C and is running on several machines. The most remarkable feature of SETHEO is its performance of up to 70 Klips on a SUN SPARC station 1 with 12 Mips. The paper comprises the theoretical background, the system architecture as well as details of the implementation.
