LPAR
2010
Springer
13 years 8 months ago
2010
Springer
The Inst-Gen-Eq method is an instantiation-based calculus which is complete for first-order clause logic modulo equality. Its distinctive feature is that it combines first-order ...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
Abstract. We study the complexity of model expansion (MX), which is the problem of expanding a given finite structure with additional relations to produce a finite model of a giv...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
Induction proofs often fail because the stated theorem is noninductive, in which case the user must strengthen the theorem or prove auxiliary properties before performing the induc...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
Ford has introduced a non-monotonic logic, System LS, inspired by an empirical study of human non-monotonic reasoning. We define here a defeasible logic FDL based on Ford’s logi...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
Termination of recursive functions is an important property in proof assistants based on dependent type theories; it implies consistency and decidability of type checking. Type-bas...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
Abstract. In this paper we study the problem of solving hard propositional satisfiability problem (SAT) instances in a computing grid or cloud, where run times and communication b...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
We consider two-player zero-sum games on graphs. On the basis of the information available to the players these games can be classified as follows: (a) partial-observation (both p...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
We address the problem of merging qualitative constraint networks (QCNs) representing agents local preferences or beliefs on the relative position of spatial or temporal entities. ...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
Abstract. We develop and analyze clause elimination procedures, a specific family of simplification techniques for conjunctive normal form (CNF) formulas. Extending known procedu...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer