Catálogo de publicaciones - libros

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 signature guarantees, while type coercion allows using terms of a more general type where the signature calls for a more special one. These operations are important e.g. in the specification and verification of object-oriented programs. We present a tableau calculus for this logic and prove its completeness.

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 similar to formulae of automaton propositional dynamic logic. Our calculus is cut-free and has the analytic superformula property so it gives a decision procedure. We show that the known EXPTIME upper bound for regular grammar logics can be obtained using our tableau calculus. We also give an effective Craig interpolation lemma for regular grammar logics using our calculus.

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 these clauses that can be shown to be propositionally unsatisfiable. In recent years, this approach has been refined in several directions, leading to both tableau-based methods, such as the , and saturation-based methods, such as and . We investigate the relationship between these calculi and answer the question to what extent refutation or consistency proofs in one calculus can be simulated in another one.

The notions of meta-ontology enhance the ability to process knowledge in information systems; in particular, deals with the kinds of properties in taxonomic knowledge based on a philosophical analysis. The goal of this paper is to devise a reasoning mechanism to check the of knowledge bases, which is important for reasoning services on taxonomic knowledge. We first consider an ontological property classification that is extended to capture individual existence and time and situation dependencies. To incorporate the notion into logical reasoning, we formalize an order-sorted modal logic that involves rigidity, sortality, and three kinds of modal operators (temporal/situational/any world). The sorted expressions and modalities establish axioms with respect to properties, implying the truth of properties in different kinds of possible worlds and in varying domains in Kripke semantics. We provide a prefixed tableau calculus to test the satisfiability of such sorted modal formulas, which validates the ontological axioms of properties.

Proof search often involves a choice between alternatives which may result in redundant information once the search is complete. This behavior can manifest itself in proof search for sequent systems by the presence of redundant formulae or subformulae in a sequent for which a proof has been found. In this paper we investigate the detection and elimination of redundant parts of a provable sequent by using labels and Boolean constraints to keep track of usage information. We illustrate our ideas in propositional linear logic, but we believe the general approach is applicable to a variety of sequent systems, including other resource-sensitive logics.

In description logics (DLs), are used for defining concepts based on concrete qualities of their instances such as the weight, age, duration, and spatial extension. So-called play an important role for capturing background knowledge. It is well-known that, when combining concrete domains with GCIs, reasoning easily becomes undecidable. In this paper, we identify a general property of concrete domains that is sufficient for proving decidability of DLs with both concrete domains and GCIs. We exhibit some useful concrete domains, most notably a spatial one based on the RCC-8 relations, which have this property. Then, we present a tableau algorithm for reasoning in DLs equipped with concrete domains and GCIs.

Ordered semantic hyper-linking (OSHL) is a first-order theorem prover that tries to take advantage of the speed of propositional theorem proving techniques. It instantiates first-order clauses to ground clauses, and applies propositional techniques to these ground clauses. OSHL-U extends OSHL with rules for unit clauses to speed up the instantiation strategy. OSHL-U obtains many of the same proofs as Otter does. This shows that many first-order theorems can be obtained without true unification, so techniques used to speed up propositional provers may be applicable to them. OSHL-U, in finding proofs, also generates and stores significantly fewer clauses than resolution prover Otter on many TPTP problems. On some TPTP groups, OSHL-U finds more proofs than Otter, despite a slower inference rate.

The goal of knowledge compilation is to enable fast queries. Prior approaches had the goal of small (i.e., polynomial in the size of the initial knowledge bases) compiled knowledge bases. Typically, query-response time is linear, so that the efficiency of querying the compiled knowledge base depends on its size. In this paper, a target for knowledge compilation called the is introduced; it has the property that even if they are large they nevertheless admit fast queries. Specifically, a query can be processed in time regardless of the size of the compiled knowledge base.

We present a clausal connection calculus for first-order intuitionistic logic. It extends the classical connection calculus by adding prefixes that encode the characteristics of intuitionistic logic. Our calculus is based on a clausal matrix characterisation for intuitionistic logic, which we prove correct and complete. The calculus was implemented by extending the classical prover leanCoP. We present some details of the implementation, called ileanCoP, and experimental results.

We present a framework and a methodology to build and analyse automatic provers using the ’Descente Infinie’ induction principle. A stronger connection between different proof techniques like those based on implicit induction and saturation is established by uniformly and explicitly representing them as applications of this principle. The framework offers a clear separation between logic and computation, by the means of i) an abstract inference system that defines the maximal sets of induction hypotheses available at every step of a proof, and ii) reasoning modules that perform the computation and allow for modular design of the concrete inference rules. The methodology is applied to define a concrete implicit induction prover and analyse an existing saturation-based inference system.