Intuitionistic hybrid logic: Introduction and survey

Intuitionistic hybrid logic is hybrid modal logic over an intuitionistic logic basis instead of a classical logical basis. In this short paper we introduce intuitionistic hybrid logic and we give a survey of work in the area.     

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.     

On goal-directed provability in classical logic

One of the key features of logic programming is the notion of goal-directed provability. In intuitionistic logic, the notion of uniform proof has been used as a proof-theoretic characterization of this property. Whilst the connections between intuitionistic logic and computation are well known, there is no reason per se why a similar notion cannot be given in classical logic. In this paper we show that there are two notions of goal-directed proof in classical logic, both of which are suitably weaker than that for intuitionistic logic. We show the completeness of this class of proofs for certain fragments, which thus form logic programming languages. As there are more possible variations on the notion of goal-directed provability in classical logic, there is a greater diversity of classical logic programming languages than intuitionistic ones. In particular, we show how logic programs may contain disjunctions in this setting. This provides a proof-theoretic basis for disjunctive logic programs, as well as characterising the “disjunctive” nature of answer substitutions for such programs in terms of the provability properties of the classical connectives Λ and Λ.     

Natural Deduction for First-Order Hybrid Logic

This is a companion paper to Braüner (2004b, Journal of Logic and Computation 14, 329–353) where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural deduction system for first-order hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relations and the quantifier domains expressed by so-called geometric theories. We prove soundness and completeness and we prove a normalisation theorem. Moreover, we give an axiom system first-order hybrid logic.     

A proof–theoretic study of the correspondence of hybrid logic and classical logic

In this paper, we show the equivalence between the provability of a proof system of basic hybrid logic and that of translated formulas of the classical predicate logic with equality and explicit substitution by a purely proof–theoretic method. Then we show the equivalence of two groups of proof systems of hybrid logic: the group of labelled deduction systems and the group of modal logic-based systems.     

Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification

We characterize provability in intuitionistic logic with equality in terms of a constraint calculus. This characterization uncovers close connections between provability in intuitionistic logic with equality and solutions to simultaneous rigid E-unification. We show that the problem of existence of a sequent proof with a given skeleton is polynomial-time equivalent to simultaneous rigid E-unifiability. This gives us a proof procedure for intuitionistic logic with equality modulo simultaneous rigid E-unification. We also show that simultaneous rigid E-unifiability is polynomial-time reducible to intuitionistic logic with equality. Thus, any proof procedure for intuitionistic logic with equality can be considered as a procedure for simultaneous rigid E-unifiability. In turn, any procedure for simultaneous rigid E-unifiability gives a procedure for establishing provability in intuitionistic logic with equality.     

Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification

We characterize provability in intuitionistic logic with equality in terms of a constraint calculus. This characterization uncovers close connections between provability in intuitionistic logic with equality and solutions to simultaneous rigid E-unification. We show that the problem of existence of a sequent proof with a given skeleton is polynomial-time equivalent to simultaneous rigid E-unifiability. This gives us a proof procedure for intuitionistic logic with equality modulo simultaneous rigid E-unification. We also show that simultaneous rigid E-unifiability is polynomial-time reducible to intuitionistic logic with equality. Thus, any proof procedure for intuitionistic logic with equality can be considered as a procedure for simultaneous rigid E-unifiability. In turn, any procedure for simultaneous rigid E-unifiability gives a procedure for establishing provability in intuitionistic logic with equality.     

经典逻辑公理在模糊逻辑系统中的真度分析

对经典逻辑中的公理在Gödel系统、Lukasiewicz以及R₀系统中的真度大小进行了分析,得到了一系列深刻而有趣的结果。     

An Institutional View on Categorical Logic

We introduce a generic notion of categorical propositional logic and provide a construction of a preorder-enriched institution out of such a logic, following the Curry-Howard-Tait paradigm. The logics are speci ed as theories of a meta-logic within the logical framework LF such that institution comorphisms are obtained from theory morphisms of the meta-logic. We prove several logic-independent results including soundness and completeness theorems and instantiate our framework with a number of examples: classical, intuitionistic,linear and modal propositional logic.     

直觉线性μ-演算

线性mu-演算(μTL)是线性时序逻辑(LTL)的不动点扩展.LTL是一个便于规范和论证反应式系统的方法.μTL作为比LTL表达能力更强的逻辑,用LTL表示的性质度可由μTL表示.类似于LTL的直觉线性时序逻辑(ILTL),提出一种基于直觉解释的μTL,称为直觉μTL(IμTL).确立了IμTL和ILTL的关系,比较了它们之间的表达能力.讨论了使用IμTL与安全性质和活性描述的关系以及描述"假设-保证"规范的问题.     

认识逻辑(1):关于知识和信念的逻辑框架

知识和信念是人工智能领域研究中经常涉及到的两个重要概念。本文讨论了知识和信念的涵义与关系，定义了认识逻辑系统ＥＩ，讨论了它的语法和语义，证明了认识逻辑ＥＬ不但是可靠的而且是完备的，认为逻辑ＥＬ不但可以用来描述人类的认识过程，还可以用于对常识推理以及分布式系统的形式化描述。     

认识逻辑(2):多认识主体的认识逻辑MEL

认识逻辑ＥＬ给出了知识和信念在单一认识主体情形下的逻辑框架。本文将认识逻辑ＥＬ推广到多认识主体的情形，得到了一个可靠并且完备的系统ＭＥＬ。ＭＥＬ继承了ＥＬ的全部性质。ＭＥＬ的一个重要特点是各个认识主体的知识是可以共享的。ＭＥＬ可以作为分布式多ａｇｅｎｔ系统的逻辑基础。     

Phase semantics for a pure noncommutative linear propositional logic

We use a many-sorted language to remove commutativity from phase semantics of linear logic an show that pure noncommutative intuitionistic linear propositional logic plus two classical rules enjoys the soundness and completeness with respect to completely noncommutative phase semantics.     

A Framework for Proof Systems

Linear logic can be used as a meta-logic to specify a range of object-level proof systems. In particular, we show that by providing different polarizations within a focused proof system for linear logic, one can account for natural deduction (normal and non-normal), sequent proofs (with and without cut), and tableaux proofs. Armed with just a few, simple variations to the linear logic encodings, more proof systems can be accommodated, including proof system using generalized elimination and generalized introduction rules. In general, most of these proof systems are developed for both classical and intuitionistic logics. By using simple results about linear logic, we can also give simple and modular proofs of the soundness and relative completeness of all the proof systems we consider.     

About axiomatic systems of product fuzzy logic

 This short paper has two goals. The first is to show a new axiomatic system of product fuzzy logic with only one non-BL axiom which has only two variables. The second goal is to prove that there cannot be any axiomatic system of the product fuzzy logic with single non-BL axiom with only one variable.     

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.     

A hybrid,decidable, logic-based knowledge representation system1

The major problem with using standard first-order logic as a basis for knowledge representation systems is its undecidability. A variant of first-order tautological entailment, a simple version of relevance logic, has been developed that has decidable inference and thus overcomes this problem. However, this logic is too weak for knowledge representation and must be strengthened. One way to strengthen the logic is to create a hybrid logic by adding a terminological reasoner. This must be done with care to retain the decidability of the logic as well as its reasonable semantics. The result, a stronger decidable logic, is used in the design of a hybrid, decidable, logic-based knowledge representation system.     

Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems

We introduce a hybrid variant of a dynamic logic with continuous state transitions along differential equations, and we present a sequent calculus for this extended hybrid dynamic logic. With the addition of satisfaction operators, this hybrid logic provides improved system introspection by referring to properties of states during system evolution. In addition to this, our calculus introduces state-based reasoning as a paradigm for delaying expansion of transitions using nominals as symbolic state labels. With these extensions, our hybrid dynamic logic advances the capabilities for compositional reasoning about (semialgebraic) hybrid dynamic systems. Moreover, the constructive reasoning support for goal-oriented analytic verification of hybrid dynamic systems carries over from the base calculus to our extended calculus.     

Implementing tactics and tacticals in a higher-order logic programming language

We argue that a logic programming language with a higher-order intuitionistic logic as its foundation can be used both to naturally specify and implement tactic-style theorem provers. The language extends traditional logic programming languages by replacing first-order terms with simply-typed -terms, replacing first-order unification with higher-order unification, and allowing implication and universal quantification in queries and the bodies of clauses. Inference rules for a variety of inference systems can be naturally specified in this language. The higher-order features of the language contribute to a concise specification of provisos concerning variable occurrences in formulas and the discharge of assumptions present in many inference systems. Tactics and tacticals, which provide a framework for high-level control over search for proofs, can be directly and naturally implemented in the extended language. This framework serves as a starting point for implementing theorem provers and proof systems that can integrate many diversified operations on formulas and proofs for a variety of logics. We present an extensive set of examples that have been implemented in the higher-order logic programming language Prolog.     

混合投影时序逻辑与混合系统的形式化验证

为了描述混合系统的性质和行为，10多年来，各种时序逻辑，如Hybrid Temporal Logic等相继出现。这些时序逻辑适用于刻画混合系统的性质和规范，但不适宜表示描述系统的实现模型。本文定义了一个混合投影时序逻辑（Hybrid Projection Temporal Logic，简称HPTL），既能刻画混合系统的性质，又能表示混合系统的实现。这样，混合系统的验证就可以很方便地在统一的数学模型框架下进行。同时，给出了HPTL的基本的逻辑等价式系统和一个用HPTL进行混合系统验证的实例。