Sciweavers

TABLEAUX
2005
Springer
13 years 10 months ago
Unit Propagation in a Tableau Framework
Unit propagation is one of the most important techniques of efficient SAT solvers. Unfortunately, this technique is not directly applicable to first-order clausal tableaux. We sho...
Gernot Stenz
TABLEAUX
2005
Springer
13 years 10 months ago
The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic
The Intuitionistic Logic Theorem Proving (ILTP) Library provides a platfom for testing and benchmarking theorem provers for first-order intuitionistic logic. It includes a collect...
Thomas Raths, Jens Otten, Christoph Kreitz
TABLEAUX
2005
Springer
13 years 10 months ago
Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic
Abstract. We present a clausal connection calculus for first-order intuitionistic logic. It extends the classical connection calculus by adding prefixes that encode the character...
Jens Otten
TABLEAUX
2005
Springer
13 years 10 months ago
Pdk: The System and Its Language
This paper presents the planning system Pdk (Planning with Domain Knowledge), based on the translation of planning problems into Linear Time Logic theories, in such a way that fin...
Marta Cialdea Mayer, Carla Limongelli, Andrea Orla...
TABLEAUX
2005
Springer
13 years 10 months ago
A Tableau Algorithm for Description Logics with Concrete Domains and GCIs
In description logics (DLs), concrete domains are used for defining concepts based on concrete qualities of their instances such as the weight, age, duration, and spatial extensio...
Carsten Lutz, Maja Milicic
TABLEAUX
2005
Springer
13 years 10 months ago
A Tableau-Based Explainer for DL Subsumption
This paper describes the implementation of a tableau-based reasoning component which is capable of providing quasi natural language explanations for subsumptions within ALEHFR+ TBo...
Thorsten Liebig, Michael Halfmann
TABLEAUX
2005
Springer
13 years 10 months ago
Comparing Instance Generation Methods for Automated Reasoning
Abstract. The clause linking technique of Lee and Plaisted proves the unsatisfiability of a set of first-order clauses by generating a sufficiently large set of instances of thes...
Swen Jacobs, Uwe Waldmann
TABLEAUX
2005
Springer
13 years 10 months ago
A Tableau Calculus with Automaton-Labelled Formulae for Regular Grammar Logics
We present a sound and complete tableau calculus for the class of regular grammar logics. Our tableau rules use a special feature called automaton-labelled formulae, which are simi...
Rajeev Goré, Linh Anh Nguyen
TABLEAUX
2005
Springer
13 years 10 months ago
A Calculus for Type Predicates and Type Coercion
We extend classical first-order logic with subtyping by type predicates and type coercion. Type predicates assert that the value of a term belongs to a more special type than the ...
Martin Giese
TABLEAUX
2005
Springer
13 years 10 months ago
LoTREC: Logical Tableaux Research Engineering Companion
Olivier Gasquet, Andreas Herzig, Dominique Longin,...