LPAR
2004
Springer
14 years 5 months ago
2004
Springer
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...
LPAR
2004
Springer
14 years 5 months ago
2004
Springer
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...
LPAR
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. Matching is a basic operation extensively used in computation. Second-order matching, in particular, provides an adequate environment for expressing program transformatio...
LPAR
2004
Springer
14 years 5 months ago
2004
Springer
LPAR
2004
Springer
14 years 5 months ago
2004
Springer
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. ...
LPAR
2004
Springer
14 years 5 months ago
2004
Springer
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 ...
LPAR
2004
Springer
14 years 5 months ago
2004
Springer
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...
LPAR
2004
Springer
14 years 5 months ago
2004
Springer
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...
LPAR
2004
Springer
14 years 5 months ago
2004
Springer
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...
LPAR
2004
Springer
14 years 5 months ago
2004
Springer
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...