One of the main reasons to employ a description logic such as EL or EL++ is the fact that it has efficient, polynomial-time algorithmic properties such as deciding consistency and inferring subsumption. However, simply by adding negation of concepts to it, we obtain the expressivity of description logics whose decision procedure is {ExpTime}-complete. Similar complexity explosion occurs if we add probability assignments on concepts. To lower the resulting complexity, we instead concentrate on assigning probabilities to Axioms (GCIs). We show that the consistency detection problem for such a probabilistic description logic is NP-complete, and present a linear algebraic deterministic algorithm to solve it, using the column generation technique. We also examine and provide algorithms for the probabilistic extension problem, which consists of inferring the minimum and maximum probabilities for a new axiom, given a consistent probabilistic knowledge base.
Facultad de Informática（信息学院）；University of the Basque Country UPV/EHU（巴斯克地区大学）
Formal ontologies are axiomatizations in a logic-based formalism. The development of formal ontologies, and their important role in the Semantic Web area, is generating considerable research on the use of automated reasoning techniques and tools that help in ontology engineering. One of the main aims is to refine and to improve axiomatizations for enabling automated reasoning tools to efficiently infer reliable information. Defects in the axiomatization can not only cause wrong inferences, but can also hinder the inference of expected information, either by increasing the computational cost of…
Sound and complete axiomatizations are provided for a number of different logics involving modalities for knowledge and time. These logics arise from different choices for various parameters. All the logics considered involve the discrete time linear temporal logic operators `next' and `until' and an operator for the knowledge of each of a number of agents. Both the single agent and multiple agent cases are studied: in some instances of the latter there is also an operator for the common knowledge of the group of all agents. Four different semantic properties of agents are considered: whether …
Manipulating logic functions via majority operators recently drew the attention of researchers in computer science. For example, circuit optimization based on majority operators enables superior results as compared to traditional logic systems. Also, the Boolean satisfiability problem finds new solving approaches when described in terms of majority decisions. To support computer logic applications based on majority a sound and complete set of axioms is required. Most of the recent advances in majority logic deal only with ternary majority (MAJ- 3) operators because the axiomatization with sole…
This paper first shows that the popular axiomatic systems proposed by Nute for Lewis' conditional logics are not equivalent to Lewis' original systems. In particular, the axiom CA which is derivable in Lewis' systems is not derivable in Nute's systems. Then the paper proposes a new set of axiomatizations for Lewis' conditional logics, without using CSO, or RCEA, or the rule of interchange of logical equivalents. Instead, the new axiomatizations adopt two axioms which correspond to cautious monotonicity and cautious cut in nonmonotonic logics, respectively. Finally, the paper gives a simple res…
We consider a specific class of tree structures that can represent basic structures in linguistics and computer science such as XML documents, parse trees, and treebanks, namely, finite node-labeled sibling-ordered trees. We present axiomatizations of the monadic second-order logic (MSO), monadic transitive closure logic (FO(TC1)) and monadic least fixed-point logic (FO(LFP1)) theories of this class of structures. These logics can express important properties such as reachability. Using model-theoretic techniques, we show by a uniform argument that these axiomatizations are complete, i.e., eac…
Nominalistic Logic (NL) is a new presentation of Paul Gilmore's Intensional Type Theory (ITT) as a sequent calculus together with a succinct nominalization axiom (N) that permits names of predicates as individuals in certain cases. The logic has a flexible comprehension axiom, but no extensionality axiom and no infinity axiom, although axiom N is the key to the derivation of Peano's postulates for the natural numbers.
University of Luxemburg（卢森堡大学）；Freie Universität Berlin（柏林自由大学）
Starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. Our axiom sets have been formalized in the Isabelle/HOL interactive proof assistant, and this formalization utilizes a semantically correct embedding of free logic in classical higher-order logic. The modeling and formal analysis of our axiom sets has been significantly supported by series of experiments with automated reasoning tools integrated with Isabelle/HOL. We also address the relation of our axiom systems to…
We give the first cut-free ExpTime (optimal) tableau decision procedure for the logic CPDLreg, which extends Converse-PDL with regular inclusion axioms characterized by finite automata. The logic CPDLreg is the combination of Converse-PDL and regular grammar logic with converse. Our tableau decision procedure uses global state caching and has been designed to increase efficiency and allow various optimization techniques, including on-the-fly propagation of local and global (in)consistency.
Standard epistemic logic studies propositional knowledge, yet many other types of knowledge such as "knowing whether", "knowing what", "knowing how" are frequently and widely used in everyday life as well as academic fields. In "Conditionally Knowing What" by Wang and Fan, an axiomatization of the epistemic logic with both regular "knowing that" operator and "conditionally knowing what" operator is given. Then the decidability and complexity of this logic command our study. In this paper, we direct our attention to the arbitrary models instead of epistemic models, thus making things clearer, a…
In this paper, we present an experiment of our randomized hints strategy of automated reasoning for yielding Axiom(5) from Axiom(1)(2)(3)(4) of Infinite-Valued Lukasiewicz Logic. In the experiment, we randomly generated a set of hints with size ranging from 30 to 60 for guiding hyper-resolution based search by the theorem prover OTTER. We have successfully found the most useful hints list (with 30 clauses) among 150 * 6 hints lists. Also, we discuss a curious non-linear increase of generated clauses in deducing Axiom(5) by applying our randomized hints strategy.
The classical approach for repairing a Description Logic ontology O in the sense of removing an unwanted consequence $α$ is to delete a minimal number of axioms from O such that the resulting ontology O' does not have the consequence $α$. However, the complete deletion of axioms may be too rough, in the sense that it may also remove consequences that are actually wanted. To alleviate this problem, we propose a more gentle way of repair in which axioms are not necessarily deleted, but only weakened. On the one hand, we investigate general properties of this gentle repair method. On the other ha…
A weakly complete finitary axiomatization for EQPL (exogenous quantum propositional logic) is presented. The proof is carried out using a non trivial extension of the Fagin-Halpern-Megiddo technique together with three Henkin style completions.
We generalize intuitionistic tense logics to the multi-modal case by placing grammar logics on an intuitionistic footing. We provide axiomatizations for a class of base intuitionistic grammar logics as well as provide axiomatizations for extensions with combinations of seriality axioms and what we call "intuitionistic path axioms". We show that each axiomatization is sound and complete with completeness being shown via a typical canonical model construction.
In this book, we consider various many-valued logics: standard, linear, hyperbolic, parabolic, non-Archimedean, p-adic, interval, neutrosophic, etc. We survey also results which show the tree different proof-theoretic frameworks for many-valued logics, e.g. frameworks of the following deductive calculi: Hilbert's style, sequent, and hypersequent. We present a general way that allows to construct systematically analytic calculi for a large family of non-Archimedean many-valued logics: hyperrational-valued, hyperreal-valued, and p-adic valued logics characterized by a special format of semantics…
"Church's thesis" ($\mathsf{CT}$) as an axiom in constructive logic states that every total function of type $\mathbb{N} \to \mathbb{N}$ is computable, i.e. definable in a model of computation. $\mathsf{CT}$ is inconsistent in both classical mathematics and in Brouwer's intuitionism since it contradicts Weak König's Lemma and the fan theorem, respectively. Recently, $\mathsf{CT}$ was proved consistent for (univalent) constructive type theory. Since neither Weak König's Lemma nor the fan theorem are a consequence of just logical axioms or just choice-like axioms assumed in constructive logic, i…
Interval Temporal Logic (ITL) is an established temporal formalism for reasoning about time periods. For over 25 years, it has been applied in a number of ways and several ITL variants, axiom systems and tools have been investigated. We solve the longstanding open problem of finding a complete axiom system for basic quantifier-free propositional ITL (PITL) with infinite time for analysing nonterminating computational systems. Our completeness proof uses a reduction to completeness for PITL with finite time and conventional propositional linear-time temporal logic. Unlike completeness proofs of…
Two different paradoxes of the fuzzy logic programming system of [29] are presented. The first paradox is due to two distinct (contradictory) truth values for every ground atom of FLP, one is syntactical, the other is semantical. The second paradox concerns the cardinality of the valid FLP formulas which is found to have contradictory values: both $\aleph_0$ the cardinality of the natural numbers, and $c$, the cardinality of the continuum. The result is that CH="False" and Axiom of Choice="False". Hence, ZFC is inconsistent.
We propose four axiomatic systems for intuitionistic linear temporal logic and show that each of these systems is sound for a class of structures based either on Kripke frames or on dynamic topological systems. Our topological semantics features a new interpretation for the `henceforth' modality that is a natural intuitionistic variant of the classical one. Using the soundness results, we show that the four logics obtained from the axiomatic systems are distinct. Finally, we show that when the language is restricted to the `henceforth'-free fragment, the set of valid formulas for the relationa…
Dynamic topological logic (DTL) is a polymodal logic designed for reasoning about {\em dynamic topological systems. These are pairs (X,f), where X is a topological space and f:X->X is continuous. DTL uses a language L which combines the topological S4 modality [] with temporal operators from linear temporal logic. Recently, I gave a sound and complete axiomatization DTL* for an extension of the logic to the language L*, where <> is allowed to act on finite sets of formulas and is interpreted as a tangled closure operator. No complete axiomatization is known over L, although one proof system, w…
Dynamic Topological Logic (DTL) is a multimodal system for reasoning about dynamical systems. It is defined semantically and, as such, most of the work done in the field has been model-theoretic. In particular, the problem of finding a complete axiomatization for the full language of DTL over the class of all dynamical systems has proven to be quite elusive. Here we propose to enrich the language to include a polyadic topological modality, originally introduced by Dawar and Otto in a different context. We then provide a sound axiomatization for DTL over this extended language, and prove that i…
We introduce a family of comparative plausibility logics over neighbourhood models, generalising Lewis' comparative plausibility operator over sphere models. We provide axiom systems for the logics, and prove their soundness and completeness with respect to the semantics. Then, we introduce two kinds of analytic proof systems for several logics in the family: a multi-premisses sequent calculus in the style of Lellmann and Pattinson, for which we prove cut admissibility, and a hypersequent calculus based on structured calculi for conditional logics by Girlando et al., tailored for countermodel …
This paper presents a uniform substitution calculus for differential game logic (dGL). Church's uniform substitutions substitute a term or formula for a function or predicate symbol everywhere. After generalizing them to differential game logic and allowing for the substitution of hybrid games for game symbols, uniform substitutions make it possible to only use axioms instead of axiom schemata, thereby substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of logical variables to restrict infinitely many a…
The modal systems S1--S3 were introduced by C. I. Lewis as logics for strict implication. While there are Kripke semantics for S2 and S3, there is no known natural semantics for S1. We extend S1 by a Substitution Principle SP which generalizes a reference rule of S1. In system S1+SP, the relation of strict equivalence $φ\equivψ$ satisfies the identity axioms of R. Suszko's non-Fregean logic adapted to the language of modal logic (we call these axioms the axioms of propositional identity). This enables us to develop a framework of algebraic semantics which captures S1+SP as well as the Lewis sy…
Public announcement logic(PAL) is an extension of epistemic logic (EL) with some reduction axioms. In this paper, we propose a cut-free labelled sequent calculus for PAL, which is an extension of that for EL with sequent rules adapted from the reduction axioms. This calculus admits cut and allows terminating proof search.
Dynamic topological logic ($\mathbf{DTL}$) is a trimodal logic designed for reasoning about dynamic topological systems. It was shown by Fernández-Duque that the natural set of axioms for $\mathbf{DTL}$ is incomplete, but he provided a complete axiomatisation in an extended language. In this paper, we consider dynamic topological logic over scattered spaces, which are topological spaces where every nonempty subspace has an isolated point. Scattered spaces appear in the context of computational logic as they provide semantics for provability and enjoy definable fixed points. We exhibit the firs…
STIT (sees to it that) semantics is one of the most prominent tools in modal logic of agency, widely used among both philosophers and responsible AI scholars. STIT logic surveys the properties of agents seeing to it that some state of affairs holds without specifying concrete actions by which that state of affairs is guaranteed. In comparison with other multi-agent modal logics, the main advantage of STIT theories is expressive power. STIT logic allows to study not only statements about agents abilities to perform certain actions (as it is in variations of Coalition Logic or Propositional Dyna…
This article introduces a relatively complete proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to use axioms instead of axiom schemata, thereby substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of logical variables to restrict infinitely many axiom schema instances to sound ones, the resulting calculus adopts only a finite number of ordinar…
The paper considers epistemic properties of linear communication chains. It describes a sound and complete logical system that, in addition to the standard axioms of S5 in a multi-modal language, contains two non-trivial axioms that capture the linear structure of communication chains.
We present a logic for the reasoning about necessity and justifications which is independent from relational semantics. We choose the concept of justification -- coming from a class of "Justification Logics" (Artemov 2008, Fitting 2009) -- as the primitive notion on which the concept of necessity is based. Our axiomatization extends Suszko's non-Fregean logic SCI (Brown, Suszko 1972) by basic axioms from Justification Logic, axioms for quantification over propositions and over justifications, and some further principles. The core axiom is: $φ$ is necessarily true iff there is a justification f…
I investigate the superintuitionistic analogue of the modal logic of chequered subsets of $\mathbb{R}^\infty$ introduced by van Benthem et al. It is observed that this logic possesses the disjunction property, contains the Scott axiom, fails to contain the Kreisel-Putnam axiom and it is a sublogic of the Medvedev logic.
We add to intuitionistic logic infinitely many classical disjunctive tautologies and use the Curry--Howard correspondence to obtain typed concurrent $λ$-calculi; each of them features a specific communication mechanism, including broadcasting and cyclic message-exchange, and enhanced expressive power with respect to the $λ$-calculus. Moreover they all implement forms of code mobility. Our results provide a first concurrent computational interpretation for many propositional intermediate logics, classical logic included.
In the framework of logic labelled transition system, a variant of weak ready simulation has been presented by Lüttgen and Vogler. It has been shown that such behavioural preorder is the largest precongruence w.r.t parallel and conjunction composition satisfying desired properties. This paper offers a ground-complete axiomatization for this precongruence over processes containing no recursion in the calculus $\text{CLL}_R$. Compared with usual inference system for process calculus, in addition to axioms about process operators, such system contains a number of axioms to characterize the intera…
We introduce a two-dimensional metric (interval) temporal logic whose internal and external time flows are dense linear orderings. We provide a suitable semantics and a sequent calculus with axioms for equality and extralogical axioms. Then we prove completeness and a semantic partial cut-elimination theorem down to formulas of a certain type.
This paper introduces a new proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to rely on axioms rather than axiom schemata, substantially simplifying implementations. Instead of nontrivial schema variables and soundness-critical side conditions on the occurrence patterns of variables, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms. The static semantics of differential dynamic logic is captured ex…
Temporal logics over finite traces are not the same as temporal logics over potentially infinite traces. Roşu first proved completeness for linear temporal logic on finite traces (LTLf) with a novel coinductive axiom. We offer a different proof, with fewer, more conventional axioms. Our proof is a direct adaptation of Kröger and Merz's Henkin-Hasenjaeger-style proof. The essence of our adaption is that we "inject" finiteness: that is, we alter the proof structure to ensure that models are finite. We aim to present a thorough, accessible proof.
We address a fundamental mismatch between the combinations of dynamics that occur in cyber-physical systems and the limited kinds of dynamics supported in analysis. Modern applications combine communication, computation, and control. They may even form dynamic distributed networks, where neither structure nor dimension stay the same while the system follows hybrid dynamics, i.e., mixed discrete and continuous dynamics. We provide the logical foundations for closing this analytic gap. We develop a formal model for distributed hybrid systems. It combines quantified differential equations with qu…
Separation Logic is an effective Program Logic for proving programs that involve pointers. Reasoning with pointers becomes difficult especially when there is aliasing arising due to several pointers to a given cell location. In this paper, we try to explore the problems with aliasing through some simple examples and introduce the notion of separating conjunction as a tool to deal with it. We introduce Separation Logic as an extension of the standard Hoare Logic with the help pf a programming language that has four pointer manipulating commands. These commands perform the usual heap operations …
This article proves the completeness of an axiomatization for differential equation invariants described by Noetherian functions. First, the differential equation axioms of differential dynamic logic are shown to be complete for reasoning about analytic invariants. Completeness crucially exploits differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Cleverly chosen differential ghosts are the proof-theoretical counterpart of dark matter. They create new hypothetical state, whose relationship to the original state variabl…
We discuss about how to make a new logic with considering a slogan: \it take the inversion of what you know. \rm Suppose that we have a Gentzen-style logical system $S$. The operation to make a new logic from $S$ is the following: \it for all the axioms and rules of $S$, change the direction of all the arrows occurred in the sequents of the axiom or the rule to the opposite side. \rm We call this operation \it Stahlization. \rm We consider certain logics in this respect.
A logic program is an executable specification. For example, merge sort in pure Prolog is a logical formula, yet shows creditable performance on long linked lists. But such executable specifications are a compromise: the logic is distorted by algorithmic considerations, yet only indirectly executable via an abstract machine. This paper introduces relational programming, a method that solves the difficulty with logic programming by a separation of concerns. It requires three texts: (1) the axioms, a logical formula that specifies the problem and is not compromised by algorithmic considerations,…
The standard reasoning problem, concept satisfiability, in the basic description logic ALC is PSPACE-complete, and it is EXPTIME-complete in the presence of unrestricted axioms. Several fragments of ALC, notably logics in the FL, EL, and DL-Lite families, have an easier satisfiability problem; sometimes it is even tractable. We classify the complexity of the standard satisfiability problems for all possible Boolean and quantifier fragments of ALC in the presence of general axioms.
This paper exhibits a general and uniform method to prove completeness for certain modal fixpoint logics. Given a set Γof modal formulas of the form γ(x, p1, . . ., pn), where x occurs only positively in γ, the language L\sharp (Γ) is obtained by adding to the language of polymodal logic a connective \sharp\_γfor each γε. The term \sharp\_γ(\varphi1, . . ., \varphin) is meant to be interpreted as the least fixed point of the functional interpretation of the term γ(x, φ1, . . ., φn). We consider the following problem: given Γ, construct an axiom system which is sound and complete with respect t…
