1,721,009 research outputs found
A sequent calculus for preferential conditional logic based on neighbourhood semantics
No full textThe basic preferential conditional logic PCL, initially proposed by Burgess, finds an interest in the formalisation of both counterfactual and plausible reasoning, since it is at the same time more general than Lewis’ systems for counterfactuals and it contains as a fragment the KLM preferential logic P for default reasoning. This logic is characterised by Kripke models equipped with a ternary relational semantics that represents a comparative similarity/normality assessment between worlds, relativised to each world. It is first shown that its semantics can be equivalently specified in terms of neighbourhood models. On the basis of this alternative semantics, a new labelled calculus is given that makes use of both world and neighbourhood labels. It is shown that the calculus enjoys syntactic cut elimination and that, by adding suitable termination conditions, it provides a decision procedure
Combining negation as failure and embedded implications in logic programs
No full textAbstractIn this paper we consider a language which combines embedded hypothetical implications and negation as failure (NAF). For this language we develop a top-down query evaluation procedure, a Kripke/Kleene fixed point semantics, and a logical interpretation by means of a completion construction. As a difference with respect to other proposals, we put no restriction on the occurrences of negation by failure; in particular, programs are not required to be stratified. The operational semantics we propose is an extension to our language of Stärk's ESLDNF, and allows negative non-ground literals to be selected in a query. The fixed point semantics is a generalization of those developed by Fitting and Kunen for flat logic programs and makes use of Kleene strong three-valued logic. The completion of a program is a recursive theory interpreted in a three-valued modal logic. We prove soundness and completeness of the operational semantics with respect to both the fixed point semantics and the completion. While soundness results require no restriction, completeness results are limited by the possibility of floundering. Similarly to Stärk, we prove completeness for the class of so-called ϵ-queries, which are not subjected to floundering. Since the property of being an ϵ-query is undecidable, we give a syntactical decidable condition which ensures this property. Such a condition is a non-trivial generalization of the usual allowedness condition for flat programs
MODULAR SEQUENT CALCULI FOR INTERPRETABILITY LOGICS
No full textAn original family of labelled sequent calculi \mathsf {G3IL}<^>{\star } for classical interpretability logics is presented, modularly designed on the basis of Verbrugge semantics (a.k.a. generalised Veltman semantics) for those logics. We prove that each of our calculi enjoys excellent structural properties, namely, admissibility of weakening, contraction and, more relevantly, cut. A complexity measure of the cut is defined by extending the notion of range previously introduced by Negri w.r.t. a labelled sequent calculus for G & ouml;del-L & ouml;b provability logic, and a cut-elimination algorithm is discussed in detail. To our knowledge, this is the most extensive and structurally well-behaving class of analytic proof systems for modal logics of interpretability currently available in the literature
Towards a Rational Closure for Expressive Description Logics: The Case of SHIQ
No full textWe explore the extension of the notion of rational closure to logics lacking the finite model property, considering the logic SHIQ. We provide a semantic characterization of rational closure in SHIQ in terms of a preferential semantics, based on a finite rank characterization of minimal models. We show that the rational closure of a KB can be computed in EXPTIME based on a polynomial encoding of the rational extension of SHIQ into entailment in SHIQ. We discuss the extension of rational closure to more expressive description logics.
The research that led to the present paper was partially supported by a grant of the group GNCS of INdAM
Proof-search and countermodel generation for non-normal modal logics: The theorem prover PRONOM
No full textIn this work we present PRONOM, a theorem prover and countermodel generator for non-normal modal logics. PRONOM implements some labelled sequent calculi recently introduced for the basic system E and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. PRONOM is inspired by the methodology of leanT(A)P and is implemented in Prolog. When a modal formula is valid, then PRONOM computes a proof (a closed tree) in the labelled calculi having a sequent with an empty left-hand side and containing only that formula on the right-hand side as a root, otherwise PRONOM is able to extract a model falsifying it from an open, saturated branch. The paper shows some experimental results, witnessing that the performances of PRONOM are promising
- …
