Fibring Non-Truth-Functional Logics: Completeness Preservation

Fibring has been shown to be useful for combining logics endowed withtruth-functional semantics. However, the techniques used so far are unableto cope with fibring of logics endowed with non-truth-functional semanticsas, for example, paraconsistent logics. The first main contribution of thepaper is the development of a suitable abstract notion of logic, that mayalso encompass systems with non-truth-functional connectives, and wherefibring can still be dealt with. Furthermore, it is shown that thisextended notion of fibring preserves completeness under certain reasonableconditions. This completeness transfer result, the second main contributionof the paper, generalizes the one established in Zanardo et al. (2001) butis obtained using new techniques that explore the properties of a suitablemeta-logic (conditional equational logic) where the (possibly)non-truth-functional valuations are specified. The modal paraconsistentlogic of da Costa and Carnielli (1988) is studied in the context of this novel notionof fibring and its completeness is so established.     

The consistency of syntactical treatments of knowledge1 (How to compile quantificational modal logics into classical FOL)

The relative expressive power of a sentential operator □α is compared to that of a syntactical predicate L(‘α’) in the setting of first-order logics. Despite well-known results by Montague and by Thomason that claim otherwise, any of the so-called “modal” logics of knowledge and belief can be compiled into classical first-order logics that have a corresponding predicate on sentences. Moreover, through the use of a partial truth predicate, the standard modal axiom schemata can be translated into single sentences, making it possible to use conventional first-order logic theorem provers to directly derive results in a wide class of modal logics.     

模态逻辑推理的翻译方法

文中研究了模态逻辑推理的翻译法，即把模态逻辑公式按照一定的规则翻译成经典逻辑公式，再用传统的定理器进行推理，文中指出，该方法在理论上保持了正规命题模态逻辑的可判定性，还给出了一些试验结果，说明该方法实际可行的。     

A polynomial space construction of tree-like models for logics with local chains of modal connectives

The LA-logics (“logics with Local Agreement”) are polymodal logics defined semantically such that at any world of a model, the sets of successors for the different accessibility relations can be linearly ordered and the accessibility relations are equivalence relations. In a previous work, we have shown that every LA-logic defined with a finite set of modal indices has an NP-complete satisfiability problem. In this paper, we introduce a class of LA-logics with a countably infinite set of modal indices and we show that the satisfiability problem is PSPACE-complete for every logic of such a class. The upper bound is shown by exhibiting a tree structure of the models. This allows us to establish a surprising correspondence between the modal depth of formulae and the number of occurrences of distinct modal connectives. More importantly, as a consequence, we can show the PSPACE-completeness of Gargov's logic DALLA and Nakamura's logic LGM restricted to modal indices that are rational numbers, for which the computational complexity characterization has been open until now. These logics are known to belong to the class of information logics and fuzzy modal logics, respectively.     

Hybridizing a Logical Framework

Logical connectives familiar from the study of hybrid logic can be added to the logical framework LF, a constructive type theory of dependent functions. This extension turns out to be an attractively simple one, and maintains all the usual theoretical and algorithmic properties, for example decidability of type-checking. Moreover it results in a rich metalanguage for encoding and reasoning about a range of resource-sensitive substructural logics, analagous to the use of LF as a metalanguage for more ordinary logics.This family of applications of the language, contrary perhaps to expectations of how hybridized systems are typically used, does not require the usual modal connectives box and diamond, nor any internalization of a Kripke accessibility relation. It does, however, make essential use of distinctively hybrid connectives: universal quantifiation over worlds, truth of a proposition at a named world, and local binding of the current world. This supports the claim that the innovations of hybrid logic have independent value even apart from their traditional relationship to temporal and alethic modal logics.     

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.     

A new modal logic for reasoning about space: spatial propositional neighborhood logic

It is widely accepted that spatial reasoning plays a central role in artificial intelligence, for it has a wide variety of potential applications, e.g., in robotics, geographical information systems, and medical analysis and diagnosis. While spatial reasoning has been extensively studied at the algebraic level, modal logics for spatial reasoning have received less attention in the literature. In this paper we propose a new modal logic, called spatial propositional neighborhood logic (SpPNL for short) for spatial reasoning through directional relations. We study the expressive power of SpPNL, we show that it is able to express meaningful spatial statements, we prove a representation theorem for abstract spatial frames, and we devise a (non-terminating) sound and complete tableaux-based deduction system for it. Finally, we compare SpPNL with the well-known algebraic spatial reasoning system called rectangle algebra.      

Uniform semantic treatment of default and autoepistemic logics

We revisit the issue of epistemological and semantic foundations for autoepistemic and default logics, two leading formalisms in nonmonotonic reasoning. We develop a general semantic approach to autoepistemic and default logics that is based on the notion of a belief pair and that exploits the lattice structure of the collection of all belief pairs. For each logic, we introduce a monotone operator on the lattice of belief pairs. We then show that a whole family of semantics can be defined in a systematic and principled way in terms of fixpoints of this operator (or as fixpoints of certain closely related operators). Our approach elucidates fundamental constructive principles in which agents form their belief sets, and leads to approximation semantics for autoepistemic and default logics. It also allows us to establish a precise one-to-one correspondence between the family of semantics for default logic and the family of semantics for autoepistemic logic. The correspondence exploits the modal interpretation of a default proposed by Konolige. Our results establish conclusively that default logic can be viewed as a fragment of autoepistemic logic, a result that has been long anticipated. At the same time, they explain the source of the difficulty to formally relate the semantics of default extensions by Reiter and autoepistemic expansions by Moore. These two semantics occupy different locations in the corresponding families of semantics for default and autoepistemic logics.     

Modal logic as metalogic

The goal of this paper is to show how modal logic may be conceived as recording the derived rules of a logical system in the system itself. This conception of modal logic was propounded by Dana Scott in the early seventies. Here, similar ideas are pursued in a context less classical than Scott's.First a family of propositional logical systems is considered, which is obtained by gradually adding structural rules to a variant of the nonassociative Lambek calculus. In this family one finds systems that correspond to the associative Lambek calculus, linear logic, relevant logics, BCK logic and intuitionistic logic. Above these basic systems, sequent systems parallel to the basic systems are constructed, which formalize various notions of derived rules for the basic systems. The deduction theorem is provable for the basic systems if, and only if, they are at least as strong as systems corresponding to linear logic, or BCK logic, depending on the language, and their deductive metalogic is not stronger than they are.However, though we do not always have the deduction theorem, we may always obtain a modal analogue of the deduction theorem for conservative modal extensions of the basic systems. Modal postulates which are necessary and sufficient for that are postulates of S4 plus modal postulates which mimic structural rules. For example, the modal postulates which Girard has recently considered in linear logic are necessary and sufficient for the modal analogue of the deduction theorem.All this may lead towards results about functional completeness in categories. When functional completeness, which is analogous to the deduction theorem, fails, we may perhaps envisage a modal analogue of functional completeness in a modal category, of which our original category is a full subcategory.     

Łukasiewicz 命题逻辑中命题的Borel 概率真度理论和极限定理

通过视赋值集为通常乘积拓扑空间,利用其上的Borel概率测度在n值及连续值■ukasiewicz命题逻辑系统中引入了命题的Borel概率真度概念,讨论了它的基本性质,特别是给出了n值情形中概率真度函数的积分表示定理,并得到了其与连续情形概率真度函数之间关系的一个极限定理.结果表明,计量逻辑学中命题的真度概念只是所研究工作的一个特例,因而基于概率真度概念可以为不确定性推理建立一种更为宽泛的计量化模型.     

Reasoning about ignorance and contradiction: many-valued logics versus epistemic logic

This paper tries to reinterpret three- and four-valued logics of partial ignorance and contradiction in the light of epistemic logic. First, we try to cast Kleene three-valued logic in the setting of a simplified form of epistemic logic. It is a two-tiered logic that embeds propositional logic into another propositional setting. The use of modalities enables Kleene truth values to be expressed at the syntactic level. Kleene logic is then a fragment of the simplified epistemic logic where modalities are in front of literals only. Kleene truth-tables can then be retrieved, while preserving tautologies of classical logic. Kleene logic connectives can be seen as set-valued extensions of Boolean logic ones, but the compositionality of Kleene logic leads to a lack of expressiveness and inferential power compared to the proposed epistemic logic. This methodology is then extended to Belnap four-valued logic, which is tailored to the handling of inconsistent information from various sources. A non-regular modal setting for reasoning about contradiction is obtained, where the adjunction law does not hold. It is a special case of a fragment of the monotonic modal logic EMN.     

A note on assumptions about Skolem functions

Skolemization is not an equivalence preserving transformation. For the purposes of refutational theorem proving it is sufficient that skolemization preserves satisfiability and unsatisfiability. Therefore there is sometimes some freedom in interpreting Skolem functions in a particular way. We show that in certain cases it is possible to exploit this freedom for simplifying formulae considerably. Examples for cases where this occurs systematically are the relational translation from modal logics to predicate logic and the relativization of first-order logics with sorts.     

Elementary Definability and Completeness in General and Positive Modal Logic

The paper generalises Goldblatt's completeness proof for Lemmon–Scott formulas to various modal propositional logics without classical negation and without ex falso, up to positive modal logic, where conjunction and disjunction, andwhere necessity and possibility are respectively independent.Further the paper proves definability theorems for Lemmon–Scottformulas, which hold even in modal propositional languages without negation and without falsum. Both, the completeness theorem and the definability theoremmake use only of special constructions of relations,like relation products. No second order logic, no general frames are involved.     

一种新的类BAN逻辑模态语义模型--兼论类BAN逻辑的语法缺陷

由于类BAN逻辑缺乏明确而清晰的语义,其语法规则和推理的正确性就受到了质疑。本文定义了安全协议的计算模型,在此基础上定义了符合模态逻辑的类BAN逻辑“可能世界”语义模型,并从语义的角度证明了在该模型下的类BAN逻辑语法存在的缺陷,同时,指出了建立或改进类BAN逻辑的方向。     

Metalogical Frameworks II: Developing a Reflected Decision Procedure

Proving theorems is a creative act demanding new combinations of ideas and on occasion new methods of argument. For this reason, theorem proving systems need to be extensible. The provers should also remain correct under extension, so there must be a secure mechanism for doing this. The tactic-style provers pioneered by Edinburgh LCF provide a very effective way to achieve secure extensions, but in such systems, all new methods must be reduced to tactics. This is a drawback because there are other useful proof generating tools such as decision procedures; these include, for example, algorithms which reduce a deduction problem, such as arithmetic provability, to a computation on graphs.The Nuprl system pioneered the combination of fixed decision procedures with tactics, but the issue of securely adding new ones was not solved. In this paper we show how to safely include user- defined decision procedures in theorem provers. The idea is to prove properties of the procedure inside the prover's logic and then invoke a reflection rule to connect the procedure to the system. We also show that using a rich underlying logic permits an abstract account of the approach so that the results carry over to different implementations and other logics.     

Presenting functors on many-sorted varieties and applications

This paper studies several applications of the notion of a presentation of a functor by operations and equations. We show that the technically straightforward generalisation of this notion from the one-sorted to the many-sorted case has several interesting consequences. First, it can be applied to give equational logic for the binding algebras modelling abstract syntax. Second, it provides a categorical approach to algebraic semantics of first-order logic. Third, this notion links the uniform treatment of logics for coalgebras of an arbitrary type T with concrete syntax and proof systems. Analysing the many-sorted case is essential for modular completeness proofs of coalgebraic logics.     

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.     

Resource Graphs and Countermodels in Resource Logics

In this abstract we emphasize the role of a semantic structure called resource graph in order to study the provability in some resource-sensitive logics, like the Bunched Implications Logic (BI) or the Non-commutative Logic (NL). Such a semantic structure is appropriate for capturing the particular interactions between different kinds of connectives (additives and multiplicatives in BI, commutatives and non-commutatives in NL) that occur during proof-search and is also well-suited for providing countermodels in case of non-provability. We illustrate the key points with a tableau method with labels and constraints for BI and then present tools, namely BILL and CheckBI, which are respectively dedicated to countermodel generation and verification in this logic.     

Labelled Modal Logics: Quantifiers

In previous work we gave an approach, based on labelled natural deduction, for formalizing proof systems for a large class of propositional modal logics that includes K, D, T, B, S4, S4.2, KD45, and S5. Here we extend this approach to quantified modal logics, providing formalizations for logics with varying, increasing, decreasing, or constant domains. The result is modular with respect to both properties of the accessibility relation in the Kripke frame and the way domains of individuals change between worlds. Our approach has a modular metatheory too; soundness, completeness and normalization are proved uniformly for every logic in our class. Finally, our work leads to a simple implementation of a modal logic theorem prover in a standard logical framework.