Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
LPAR
2004
Springer
10 years 7 months ago
Abstract DPLL and Abstract DPLL Modulo Theories
DPLL and DPLL Modulo Theories Robert Nieuwenhuis , Albert Oliveras , and Cesare Tinelli We introduce Abstract DPLL, a general and simple abstract rule-based formulation of the Davi...
Robert Nieuwenhuis, Albert Oliveras, Cesare Tinell...
LPAR
2004
Springer
10 years 7 months ago
Weighted Answer Sets and Applications in Intelligence Analysis
The extended answer set semantics for simple logic programs, i.e. programs with only classical negation, allows for the defeat of rules to resolve contradictions. In addition, a pa...
Davy Van Nieuwenborgh, Stijn Heymans, Dirk Vermeir
LPAR
2004
Springer
10 years 7 months ago
Second-Order Matching via Explicit Substitutions
Abstract. Matching is a basic operation extensively used in computation. Second-order matching, in particular, provides an adequate environment for expressing program transformatio...
Flávio L. C. de Moura, Fairouz Kamareddine,...
LPAR
2004
Springer
10 years 7 months ago
A Decomposition Rule for Decision Procedures by Resolution-Based Calculi
Resolution-based calculi are among the most widely used calculi for theorem proving in first-order logic. Numerous refinements of resolution are nowadays available, such as e.g. ...
Ullrich Hustadt, Boris Motik, Ulrike Sattler
LPAR
2004
Springer
10 years 7 months ago
The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs
The dependency pair approach is one of the most powerful techniques for automated termination proofs of term rewrite systems. Up to now, it was regarded as one of several possible ...
Jürgen Giesl, René Thiemann, Peter Sch...
LPAR
2004
Springer
10 years 7 months ago
Nonmonotonic Description Logic Programs: Implementation and Experiments
Abstract. The coupling of description logic reasoning systems with other reasoning formalisms (possibly over the Web) is becoming an important research issue and calls for advanced...
Thomas Eiter, Giovambattista Ianni, Roman Schindla...
LPAR
2004
Springer
10 years 7 months ago
The Inverse Method for the Logic of Bunched Implications
Abstract. The inverse method, due to Maslov, is a forward theorem proving method for cut-free sequent calculi that relies on the subformula property. The Logic of Bunched Implicati...
Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, S...
LPAR
2004
Springer
10 years 7 months ago
Evaluating QBFs via Symbolic Skolemization
Abstract. We describe a novel decision procedure for Quantified Boolean Formulas (QBFs) which aims to unleash the hidden potential of quantified reasoning in applications. The Sk...
Marco Benedetti
LPAR
2004
Springer
10 years 7 months ago
Uniform Rules and Dialogue Games for Fuzzy Logics
Abstract. We provide uniform and invertible logical rules in a framework of relational hypersequents for the three fundamental t-norm based fuzzy logics i.e., Łukasiewicz logic, G...
Agata Ciabattoni, Christian G. Fermüller, Geo...
books