Phase Semantics and Petri Net Interpretation for Resource-Sensitive Strong Negation

Wansing’s extended intuitionistic linear logic with strong negation, called WILL, is regarded as a resource-conscious refinment of Nelson’s constructive logics with strong negation. In this paper, (1) the completeness theorem with respect to phase semantics is proved for WILL using a method that simultaneously derives the cut-elimination theorem, (2) a simple correspondence between the class of Petri nets with inhibitor arcs and a fragment of WILL is obtained using a Kripke semantics, (3) a cut-free sequent calculus for WILL, called twist calculus, is presented, (4) a strongly normalizable typed λ-calculus is obtained for a fragment of WILL, and (5) new applications of WILL in medical diagnosis and electric circuit theory are proposed. Strong negation in WILL is found to be expressible as a resource-conscious refutability, and is shown to correspond to inhibitor arcs in Petri net theory.     

Representing model theory in a type-theoretical logical framework

In a broad sense, logic is the field of formal languages for knowledge and truth that have a formal semantics. It tends to be difficult to give a narrower definition because very different kinds of logics exist. One of the most fundamental contrasts is between the different methods of assigning semantics. Here two classes can be distinguished: model theoretical semantics based on a foundation of mathematics such as set theory, and proof theoretical semantics based on an inference system possibly formulated within a type theory.Logical frameworks have been developed to cope with the variety of available logics unifying the underlying ontological notions and providing a meta-theory to reason abstractly about logics. While these have been very successful, they have so far focused on either model or proof theoretical semantics. We contribute to a unified framework by showing how the type/proof theoretical Edinburgh Logical Framework (LF) can be applied to the representation of model theoretical logics.We give a comprehensive formal representation of first-order logic, covering both its proof and its model theoretical semantics as well as its soundness in LF. For the model theory, we have to represent the mathematical foundation itself in LF, and we provide two solutions for that. Firstly, we give a meta-language that is strong enough to represent the model theory while being simple enough to be treated as a fragment of untyped set theory. Secondly, we represent Zermelo-Fraenkel set theory and show how it subsumes our meta-language. Specific models are represented as LF morphisms.All representations are given in and mechanically verified by the Twelf implementation of LF. Moreover, we use the Twelf module system to treat all connectives and quantifiers independently. Thus, individual connectives are available for reuse when representing other logics, and we obtain the first version of a feature library from which logics can be pieced together.Our results and methods are not restricted to first-order logic and scale to a wide variety of logical systems, thus demonstrating the feasibility of comprehensively formalizing large scale representation theorems in a logical framework.     

Combining and automating classical and non-classical logics in classical higher-order logics

Numerous classical and non-classical logics can be elegantly embedded in Church??s simple type theory, also known as classical higher-order logic. Examples include propositional and quantified multimodal logics, intuitionistic logics, logics for security, and logics for spatial reasoning. Furthermore, simple type theory is sufficiently expressive to model combinations of embedded logics and it has a well understood semantics. Off-the-shelf reasoning systems for simple type theory exist that can be uniformly employed for reasoning within and about embedded logics and logics combinations. In this article we focus on combinations of (quantified) epistemic and doxastic logics and study their application for modeling and automating the reasoning of rational agents. We present illustrating example problems and report on experiments with off-the-shelf higher-order automated theorem provers.     

Display Calculi for Logics with Relative Accessibility Relations

We define cut-free display calculi for knowledge logics wherean indiscernibility relation is associated to each set of agents, andwhere agents decide the membership of objects using thisindiscernibility relation. To do so, we first translate the knowledgelogics into polymodal logics axiomatised by primitive axioms and thenuse Kracht's results on properly displayable logics to define thedisplay calculi. Apart from these technical results, we argue thatDisplay Logic is a natural framework to define cut-free calculi for manyother logics with relative accessibility relations.     

A Sequent Calculus for Subtyping Polymorphic Types

We present two complete systems for polymorphic types with sub- typing. One system is in the style of natural deduction, while another is a Gentzen-style sequent calculus system. We prove several meta- mathematical properties for these systems including cut elimination, subject reduction, coherence, and decidability of type reconstruction. Following the approach by J. Mitchell, the sequents are given a simple semantics using logical relations over applicative structures. The systems are complete with respect to this semantics. The logic which emerges from this paper can be seen as a successor to the original Hilbert style system proposed by J. Mitchell in 1988, and to the “half way” sequent calculus of G. Longo, K. Milsted, and S. Soloviev proposed in 1995.     

Cut-free sequent systems for temporal logic

Currently known sequent systems for temporal logics such as linear time temporal logic and computation tree logic either rely on a cut rule, an invariant rule, or an infinitary rule. The first and second violate the subformula property and the third has infinitely many premises. We present finitary cut-free invariant-free weakening-free and contraction-free sequent systems for both logics mentioned. In the case of linear time all rules are invertible. The systems are based on annotating fixpoint formulas with a history, an approach which has also been used in game-theoretic characterisations of these logics.     

On the formal semantics of IF-like logics

In classical logics, the meaning of a formula is invariant with respect to the renaming of bound variables. This property, normally taken for granted, has been shown not to hold in the case of Independence Friendly (IF) logics. In this paper we argue that this is not an inherent characteristic of these logics but a defect in the way in which the compositional semantics given by Hodges for the regular fragment was generalized to arbitrary formulas. We fix this by proposing an alternative formalization, based on a variation of the classical notion of valuation. Basic metatheoretical results are proven. We present these results for Hodges' slash logic (from which these can be easily transferred to other IF-like logics) and we also consider the flattening operator, for which we give novel game-theoretical semantics.     

Cut-free proof systems for logics of weak excluded middle

 In this work we perform a proof-theoretical investigation of some logical systems in the neighborhood of substructural, intermediate and many-valued logics. The common feature of the logics we consider is that they satisfy some weak forms of the excluded-middle principle. We first propose a cut-free hypersequent calculus for the intermediate logic LQ, obtained by adding the axiom *A∨**A to intuitionistic logic. We then propose cut-free calculi for systems W _n , obtained by adding the axioms *A∨(A ⊕ ⋯ ⊕ A) (n−1 times) to affine linear logic (without exponential connectives). For n=3, the system W _n coincides with 3-valued Łukasiewicz logic. For n>3, W _n is a proper subsystem of n-valued Łukasiewicz logic. Our calculi can be seen as a first step towards the development of uniform cut-free Gentzen calculi for finite-valued Łukasiewicz logics.     

Multi-modal nonmonotonic logics of minimal knowledge

In this paper we introduce multi-modal logics of minimal knowledge. Such a family of logics constitutes the first proposal in the field of epistemic nonmonotonic logic in which the three following aspects are simultaneously addressed: (1) the possibility of formalizing multiple agents through multiple modal operators; (2) the possibility of using first-order quantification in the modal language; (3) the possibility of formalizing nonmonotonic reasoning abilities for the agents modeled, based on the principle of minimal knowledge. We illustrate the expressive capabilities of multi-modal logics of minimal knowledge to provide a formal semantics to peer-to-peer data integration systems, which constitute one of the most recent and complex architectures for distributed information systems.      

纤维逻辑

形式逻辑已经从简单命题逻辑发展到比较复杂的模态逻辑系列。但是在主体环境下，已有逻辑的复杂性仍然不能有效刻画主体复杂的心智。有一些人工智能研究者根据主体心智的多重性，在模态逻辑中引入多种模态算子，并借此对主体加以刻画。但是原来的可能世界语义却难以容纳如此复杂的语法，出现了很多不合理的地方。本文首先介绍了新近出现的纤维逻辑（fibring logics），然后归纳了目前将此理论应用在主体BDI建模的研究现状，最后分析纤维逻辑的不足之处，讨论了其他可能的应用，并对今后的工作做了展望。     

Proving the Asymmetry Thesis Principles for a BDI Agent-Oriented Programming Language

In this paper, we consider each of the nine principles of BDI logics as defined by Rao and Georgeff based on Bratman's asymmetry thesis, and we verify which ones are satisfied by Rao's AgentSpeak(L), a computable logic language inspired by the BDI architecture for cognitive agents. This is in line with Rao's original motivation for defining AgentSpeak(L): to bridge the gap between the theory and practice of BDI agent systems. In order to set the grounds for the proof, we first introduce a particular way in which to define the informational, motivational, and deliberative modalities of BDI logics for AgentSpeak(L) agents, according to its structural operational semantics (that we introduced in a recent paper). This provides a framework that can be used to investigate further properties of AgentSpeak(L) agents, contributing towards giving firm theoretical grounds for BDI agent programming.     

Equivalential Structures for Binary and Ternary Syllogistics

The aim of this paper is to provide a contribution to the natural logic program which explores logics in natural language. The paper offers two logics called \( \mathcal {R}(\forall ,\exists ) \) and \( \mathcal {G}(\forall ,\exists ) \) for dealing with inference involving simple sentences with transitive verbs and ditransitive verbs and quantified noun phrases in subject and object position. With this purpose, the relational logics (without Boolean connectives) are introduced and a model-theoretic proof of decidability for they are presented. In the present paper we develop algebraic semantics (bounded meet semi-lattice) of the logics using congruence theory.     

On structuring proof search for first order linear logic

Full first-order linear logic can be presented as an abstract logic programming language in Miller's system Forum, which yields a sensible operational interpretation in the ‘proof search as computation’ paradigm. However, Forum still has to deal with syntactic details that would normally be ignored by a reasonable operational semantics. In this respect, Forum improves on Gentzen systems for linear logic by restricting the language and the form of inference rules. We further improve on Forum by restricting the class of formulae allowed, in a system we call G-Forum, which is still equivalent to full first-order linear logic. The only formulae allowed in G-Forum have the same shape as Forum sequents: the restriction does not diminish expressiveness and makes G-Forum amenable to proof theoretic analysis. G-Forum consists of two (big) inference rules, for which we show a cut elimination procedure. This does not need to appeal to finer detail in formulae and sequents than is provided by G-Forum, thus successfully testing the internal symmetries of our system.     

Focusing and polarization in linear,intuitionistic, and classical logics

A focused proof system provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured. Within linear logic, the focused proof system of Andreoli provides an elegant and comprehensive normal form for cut-free proofs. Within intuitionistic and classical logics, there are various different proof systems in the literature that exhibit focusing behavior. These focused proof systems have been applied to both the proof search and the proof normalization approaches to computation. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other intuitionistic proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system LKF for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard’s LC and LU proof systems.     

Characterization of Interval Fuzzy Logic Systems of Connectives by Group Transformations

The global structure of various systems of logic connectives is investigated by looking at abstract group properties of the group of transformations of these. Such characterizations of fuzzy interval logics are examined in Sections 4–9. The paper starts by introducing readers to the Checklist Paradigm semantics of fuzzy interval logics (Sections 2 and 3). In the Appendix we present some basic notions of fuzzy logics, sets and many-valued logics in order to make the paper accessible to readers not familiar with fuzzy sets.     

Preservation of Interpolation Features by Fibring

Fibring is a metalogical constructor that permits to combinedifferent logics by operating on their deductive systems undercertain natural restrictions, as for example that the two givenlogics are presented by deductive systems of the same type.Under such circumstances, fibring will produce a new deductivesystem by means of the free use of inference rules from bothdeductive systems, provided the rules are schematic, in thesense of using variables that are open for application to formulaswith new linguistic symbols (from the point of view of eachlogic component). Fibring is a generalization of fusion, a lessgeneral but wider developed mechanism which permits resultsof the following kind: if each logic component is decidable(or sound, or complete with respect to a certain semantics)then the resulting logic heirs such a property. The interestfor such preservation results for combining logics is evident,and they have been achieved in the more general setting of fibringin several cases. The Craig interpolation property and the Maeharainterpolation have a special significance when combining logics,being related to certain problems of complexity theory, someproperties of model theory and to the usual (global) metatheoremof deduction. When the peculiarities of the distinction betweenlocal and global deduction interfere, justifying what we callcareful reasoning, the question of preservation of interpolationbecomes more subtle and other forms of interpolation can bedistinguished. These questions are investigated and several(global and local) preservation results for interpolation areobtained for fibring logics that fulfill mild requirements.     

Reasoning about knowledge and belief: a survey

We examine a number of logics of knowledge and belief from the perspective of knowledge-based systems. We are concerned with the beliefs of a knowledge-based system, including both the system's base set of beliefs–those garnered directly from the world–and beliefs that follow from the base set. Three things to consider with such logics are the expressive power of the language of the logic, the correctness and completeness of the inferences sanctioned, and the speed with which it is possible to determine whether a given sentence is believed. The influential possible worlds approach to representing belief has the property of logical omniscience, which makes for inferences that are unacceptable in the context of belief and may take too much time to make. We examine a number of weak logics which attempt to deal with these problems. These logics divide into three categories: those that admit incomplete or inconsistent situations into their semantics, those that posit a number of distinct states for a believer which correspond roughly to frames of mind, and those that incorporate axioms or other syntactic entities directly into the semantics. As to expressive power, we consider whether belief should be represented by a predicate or a sentential operator and examine the boundary between self-referential and inconsistent systems. Finally, we consider logics of believing only , which add the assumption that a system's base set of beliefs are, in a certain sense, all that it believes.     

A decidable first-order logic for knowledge representation

Decidable first-order logics with reasonable model-theoretic semantics have several benefits for knowledge representation. These logics have the expressive power of standard first order logic along with an inference algorithm that will always terminate, both important considerations for knowledge representation. Knowledge representation systems that include a faithful implementation of one of these logics can also use its model-theoretic semantics to provide meanings for the data they store. One such logic, a variant of a simple type of first-order relevance logic, is developed and its properties described. This logic, although extremely weak, does capture a non-trivial and well-motivated set of inferences that can be entrusted to a knowledge representation system.This is a revised and much extended version of a paper of the same name that appears in the Proceedings of the Ninth International Joint Conference on Artificial Intelligence, Los Angeles, California, 1985.     

A generic complete dynamic logic for reasoning about purity and effects

For a number of programming languages, among them Eiffel, C, Java, and Ruby, Hoare-style logics and dynamic logics have been developed. In these logics, pre- and postconditions are typically formulated using potentially effectful programs. In order to ensure that these pre- and postconditions behave like logical formulae (that is, enjoy some kind of referential transparency), a notion of purity is needed. Here, we introduce a generic framework for reasoning about purity and effects. Effects are modelled abstractly and axiomatically, using Moggi’s idea of encapsulation of effects as monads. We introduce a dynamic logic (from which, as usual, a Hoare logic can be derived) whose logical formulae are pure programs in a strong sense. We formulate a set of proof rules for this logic, and prove it to be complete with respect to a categorical semantics. Using dynamic logic, we then develop a relaxed notion of purity which allows for observationally neutral effects such writing on newly allocated memory.