Catálogo de publicaciones - libros

CERES is a method for cut-elimination in classical logic which is based on resolution. In this paper we extend CERES to CERES-m, a resolution-based method of cut-elimination in Gentzen calculi for arbitrary finitely-valued logics. Like in the classical case the core of the method is the construction of a resolution proof in finitely-valued logics. Compared to Gentzen-type cut-elimination methods the advantage of CERES-m is a twofold one: 1. it is easier to define and 2. it is computationally superior and thus more appropriate for implementations and experiments.

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. , a calculus highly optimized for theorem proving with equality. However, even such an advanced calculus does not restrict inferences enough to obtain decision procedures for complex logics, such as . In this paper, we present a new inference rule, which can be combined with any resolution-based calculus compatible with the standard notion of redundancy. We combine decomposition with basic superposition to obtain three new decision procedures: () for the description logic , () for the description logic , and () for answering conjunctive queries over knowledge bases. The first two procedures are worst-case optimal and, based on the vast experience in building efficient theorem provers, we expect them to be suitable for practical usage.

We introduce , a general and simple abstract rule-based formulation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure. Its properties, such as soundness, completeness or termination, immediately carry over to the modern DPLL implementations with features such as non-chronological backtracking or clause learning. This allows one to formally reason about practical DPLL algorithms in a simple way. In the second part of this paper we extend the framework to . This allows us to express—and formally reason about—state-of-the-art concrete DPLL-based techniques for satisfiability modulo background theories, such as the different approaches, or our DPLL(T) framework.

In program verification one has often to reason about lists over elements of a given nature. Thus, it becomes important to be able to combine the theory of lists with a generic theory modeling the elements. This combination can be achieved using the Nelson-Oppen method is stably infinite.

The goal of this paper is to relax the stable-infiniteness requirement. More specifically, we provide a new method that is able to combine the theory of lists with any theory of the elements, regardless of whether is stably infinite or not. The crux of our combination method is to guess an arrangement over a set of variables that is larger than the one considered by Nelson and Oppen.

Furthermore, our results entail that it is also possible to combine with the more general theory of lists with a length function.

Abstract model generation refers to model generation for abstract clause sets in which arguments of atoms are ignored. We give two abstract clause sets which are obtained from normal clause sets. One is for checking satisfiability of the original normal clause set. Another is used for eliminating unnecessary clauses from the original one. These abstract clause sets are propositional, i.e. decidable. Thus, we can use them for preprocessing the original one.

Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class of first order clauses, which extends the Skolem class. They showed its satisfiability problem to be in 3-DEXPTIME. We improve this result by showing that satisfiability for this class is NEXPTIME-complete, using new resolution techniques. We show satisfiability to be DEXPTIME-complete if clauses are Horn, which is what is required for modeling cryptographic protocols. While translation to Horn clauses only gives a DEXPTIME upper bound for the secrecy problem for these protocols, we further show that this secrecy problem is actually DEXPTIME-complete.

There is a trend to study extended variants of propositional logic which have explicit means to represent cardinality constraints. That is accomplished using so-called c-atoms. We show that c-atoms can be efficiently reduced to a general form of Exact Satisfiability. The general problem is to find an assignment for a CNF such that exactly literals are true in each clause for any ≥ 1. We show that this problem is solvable in time (1.4143) (where is the number of variables) regardless of if we allow exponential space. For polynomial space, we present an algorithm solving for all strictly better than the trivial (2) bound. For =2, =3 and =4 we obtain upper time bounds in (1.5157), (1.6202) and (1.6844), respectively. We also present a dedicated algorithm running in polynomial space and time (1.4511).

We present BCiC, a system for verifying and authenticating code that combines language-based proof methods with public-key digital signatures. BCiC aims to augment the rigor of formal proofs about intrinsic properties of code by relying on authentication and trust relations. BCiC integrates the Binder security language with the Calculus of (Co)Inductive Constructions (CiC). In this respect, it is a descendant of our previous logic BLF, which was based on LF rather than CiC. This paper focuses on the architecture and implementation of BCiC. In addition to a logical inference engine, the design most notably includes a network communication module for the efficient exchange of logical facts between hosts, and a cryptography module for generating and checking signatures. The implementation cooperates with the Open Verifier, a state-of-the-art system for proof-carrying code with modular checkers.

The hybrid logic is obtained by adding nominals and the satisfaction operator @ to the basic modal logic. The resulting logic gains expressive power without increasing the complexity of the satisfiability problem, which remains within PSpace. A resolution calculus for was introduced in [5], but it did not provide strategies for ordered resolution and selection functions. Additionally, the problem of termination was left open.

In this paper we address both issues. We first define proper notions of admissible orderings and selection functions and prove the refutational completeness of the obtained ordered resolution calculus using a standard “candidate model” construction [10]. Next, we refine some of the nominal-handling rules and show that the resulting calculus is sound, complete and can only generate a finite number of clauses, establishing termination. Finally, the theoretical results were tested empirically by implementing the new strategies into HyLoRes [6,18], an experimental prototype for the original calculus described in [5]. Both versions of the prover were compared and we discuss some preliminary results.

We observe, that subsumption of clauses (in the language of first order logic), so far understood as a syntactic notion, can also be defined by semantical means. Subsumption is NP-complete and testing subsumption takes roughly half of the running time of a typical first order resolution-based theorem prover. We also give some experimental evidence, that replacing syntactic indexing for subsumption by our semantic Monte Carlo technique can, in some situations, significantly decrease the cost of subsumption testing.

Finally, we provide some evidence that a similar semantic idea can be probably successfully used for testing for AC matching, which is another NP-complete problem whose millions of instances are being solved by theorem provers.