A fuzzy logic for an ordinal sum t-norm

Among the class of residuated fuzzy logics, a few of them have been shown to have standard completeness both for propositional and predicate calculus, like Gödel, NM and monoidal t-norm-based logic systems. In this paper, a new residuated logic NMG, which aims at capturing the tautologies of a class of ordinal sum t-norms and their residua, is introduced and its standard completeness both for propositional calculus and for predicate calculus are proved.     

Extracting BB′IW Inhabitants of Simple Types From Proofs in the Sequent Calculus {LT_\to^{t}} for Implicational Ticket Entailment

The decidability of the logic of pure ticket entailment means that the problem of inhabitation of simple types by combinators over the base { B, B′, I, W } is decidable too. Type-assignment systems are often formulated as natural deduction systems. However, our decision procedure for this logic, which we presented in earlier papers, relies on two sequent calculi and it does not yield directly a combinator for a theorem of ${T_\to}$ . Here we describe an algorithm to extract an inhabitant from a sequent calculus proof—without translating the proof into another proof system.     

强正则剩余格值逻辑系统（L）N及其完备性

正则剩余格是一类重要的模糊逻辑代数系统,而常见的模糊逻辑形式系统大多数带有非联接词,并且相应的Lindenbaum代数都是正则剩余格.本文以强正则剩余格为语义,建立了一个一般的命题演算形式系统LN,并且证明了这个系统的完备性.几种常见的带有非联接词的模糊逻辑形式系统都是系统LN的扩张.     

强正则剩余格值逻辑系统L~N及其完备性

正则剩余格是一类重要的模糊逻辑代数系统,而常见的模糊逻辑形式系统大多数带有非联接词,并且相应的Lindenbaum代数都是正则剩余格.本文以强正则剩余格为语义,建立了一个一般的命题演算形式系统LN,并且证明了这个系统的完备性.几种常见的带有非联接词的模糊逻辑形式系统都是系统LN的扩张.     

Diagonal fixed points in algebraic recursion theory

The relation between least and diagonal fixed points is a well known and completely studied question for a large class of partially ordered models of the lambda calculus and combinatory logic. Here we consider this question in the context of algebraic recursion theory, whose close connection with combinatory logic recently become apparent. We find a comparatively simple and rather weak general condition which suffices to prove the equality of least fixed points with canonical (corresponding to those produced by the Curry combinator in lambda calculus) diagonal fixed points in a class of partially ordered algebras which covers both combinatory spaces of Skordev and operative spaces of Ivanov. Especially, this yields an essential improvement of the axiomatization of recursion theory via combinatory spaces. Supported in part by the Ministry of Education and Science of Republic of Bulgaria, contract No 705     

A normalizing system of natural deduction for intuitionistic linear logic

 The main result of this paper is a normalizing system of natural deduction for the full language of intuitionistic linear logic. No explicit weakening or contraction rules for -formulas are needed. By the systematic use of general elimination rules a correspondence between normal derivations and cut-free derivations in sequent calculus is obtained. Normalization and the subformula property for normal derivations follow through translation to sequent calculus and cut-elimination. Received: 10 October 2000 / Revised version: 26 July 2001 / Published online: 2 September 2002 Mathematics Subject Classification (2000): 03F52, 03F05 Keywords or phrases: Linear logic – Natural deduction – General elimination rules     

Axiomatizations of team logics

In a modular approach, we lift Hilbert-style proof systems for propositional, modal and first-order logic to generalized systems for their respective team-based extensions. We obtain sound and complete axiomatizations for the dependence-free fragment FO(～) of Väänänen's first-order team logic TL, for propositional team logic PTL, quantified propositional team logic QPTL, modal team logic MTL, and for the corresponding logics of dependence, independence, inclusion and exclusion.As a crucial step in the completeness proof, we show that the above logics admit, in a particular sense, a semantics-preserving elimination of modalities and quantifiers from formulas.     

The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions

The Gödel-McKinsey-Tarski embedding allows to view intuitionistic logic through the lenses of modal logic. In this work, an extension of the modal embedding to infinitary intuitionistic logic is introduced. First, a neighborhood semantics for a family of axiomatically presented infinitary modal logics is given and soundness and completeness are proved via the method of canonical models. The semantics is then exploited to obtain a labelled sequent calculus with good structural properties. Next, soundness and faithfulness of the embedding are established by transfinite induction on the height of derivations: the proof is obtained directly without resorting to non-constructive principles. Finally, the modal embedding is employed in order to relate classical, intuitionistic and modal derivability in infinitary logic extended with axioms.     

Positive Frege and its Scott‐style semantics

We show that the untyped λ ‐calculus can be extended with Frege's interpretation of propositional notions, provided we restrict β ‐conversion to positive expressions. The system of illative λ ‐calculus so obtained admits a natural Scott‐style semantics. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

A Sequent Calculus for Propositional Dynamic Logic for Agents

We consider propositional dynamic logic for agents. For this logic, we present a sequent calculus with a restricted cut rule and prove the soundness and completeness for the calculus.     

A sequent calculus for logic of knowledge and past time: Completeness and decidability

We consider logic of knowledge and past time. This logic involves the discrete-time linear temporal operators next, until, weak yesterday, and since. In addition, it contains an indexed set of unary modal operators agent i knows.We consider the semantic constraint of the unique initial states for this logic. For the logic, we present a sequent calculus with a restricted cut rule. We prove the soundness and completeness of the sequent calculus presented. We prove the decidability of provability in the considered calculus as well. So, this calculus can be used as a basis for automated theorem proving. The proof method for the completeness can be used to construct complete sequent calculi with a restricted cut rule for this logic with other semantical constraints as well. Published in Lietuvos Matematikos Rinkinys, Vol. 46, No. 3, pp. 427–437, July–September, 2006.     

A Proof-Theoretic Semantics for Exclusion

The paper provides a proof-theory (natural deduction and sequent calculus) for a negative presentation of classical logic based on a single primitive of exclusion (of variable arity), generalizing the known presentation via the binary ‘nand. The completeness is established via deductive equivalence to Gentzens NK/LK systems.     

Inconsistency-Tolerant Bunched Implications

It is known that logical systems with the property of paraconsistency can deal with inconsistency-tolerant and uncertainty reasoning more appropriately than systems which are non-paraconsistent. It is also known that the logic BI of bunched implications is useful for formalizing resource-sensitive reasoning. In this paper, a paraconsistent extension PBI of BI is studied. The logic PBI is thus intended to formalize an appropriate combination of inconsistency-tolerant reasoning and resource-sensitive reasoning. A Gentzen-type sequent calculus SPBI for PBI is introduced, and the cut-elimination and decidability theorems for SPBI are proved. An extension of the Grothendieck topological semantics for BI is introduced for PBI, and the completeness theorem with respect to this semantics is proved.     

ON SOME INTERPRETATIONS OF CLASSICAL LOGIC

In distinction from the well-known double-negation embeddings of the classical logic we consider some variants of single-negation embeddings and describe some classes of superintuitionistic first-order predicate logics in which the classical first-order calculus is interpretable in such a way. Also we find the minimal extensions of Heyting's logic in which the classical predicate logic can be embedded by means of these translations.     

On a logic of involutive quantales

The logic just corresponding to (non‐commutative) involutive quantales, which was introduced by Wendy MacCaull, is reconsidered in order to obtain a cut‐free sequent calculus formulation, and the completeness theorem (with respect to the involutive quantale model ) for this logic is proved using a new admissible rule. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

A Sequent Calculus for Propositional Dynamic Logic for Agents with Interactions

We consider a propositional dynamic logic for agents with interactions such as known commitment, no learning, and perfect recall. For this logic, we present a sequent calculus with a restricted cut rule and prove the soundness and completeness for the calculus.__________Published in Lietuvos Matematikos Rinkinys, Vol. 45, No. 2, pp. 261–269, April–June, 2005.     

Constructive modal logics I

We often have to draw conclusions about states of machines in computer science and about states of knowledge and belief in artificial intelligence (AI) based on partial information. Nerode (1990) suggested using constructive (equivalently, intuitionistic) logic as the language to express such deductions and also suggested designing appropriate intuitionistic Kripke frames to express the partial information. Following this program, Nerode and Wijesekera (1990) developed syntax, semantics and completeness for a system of intuitionistic dynamic logic for proving properties of concurrent programs. Like all dynamics logics, this was a logic of many modalities, each expressing a program, but in intuitionistic rather than in classical logic. In that logic, both box and diamond are needed, but these two are not intuitionistically interdefinable and, worse, diamond does not distribute over ‘or’, except for sequential programs. This also happens in other contemplated computer science and AI applications, and leads outside the class of constructive logics investigated in the literature. The present paper fills this gap. We provide intuitionistic logics with independent box and diamond without assuming distribution of diamond over ‘or’. The completeness theorem is based on intuitionistic Kripke frames (partially ordered sets of increasing worlds), but equipped with an additional, quite separate accessibility relation between worlds. In the interpretation of Nerode and Wijesekera (1990), worlds under the partial order represent states of partial knowledge, the accessibility represents change in state of partial knowledge resulting from executing a specific program. But there are many other computer science interpretations. This formalism covers all computer science applications of which we are aware. We also give a cut elimination theorem and algebraic and topological formulations, since these present some new difficulties. Finally, these results were obtained prior to those in Nerode and Wijesekera (1990).     

Circular proofs for the Gödel-Löb provability logic

Sequent calculus for the provability logic GL is considered, in which provability is based on the notion of a circular proof. Unlike ordinary derivations, circular proofs are represented by graphs allowed to contain cycles, rather than by finite trees. Using this notion, we obtain a syntactic proof of the Lyndon interpolation property for GL.     

Superposition Decides the First-Order Logic Fragment Over Ground Theories

The hierarchic superposition calculus over a theory T, called SUP(T), enables sound reasoning on the hierarchic combination of a theory T with full first-order logic, FOL(T). If a FOL(T) clause set enjoys a sufficient completeness criterion, the calculus is even complete. Clause sets over the ground fragment of FOL(T) are not sufficiently complete, in general. In this paper we show that any clause set over the ground FOL(T) fragment can be transformed into a sufficiently complete one, and prove that SUP(T) terminates on the transformed clause set, hence constitutes a decision procedure provided the existential fragment of the theory T is decidable. Thanks to the hierarchic design of SUP(T), the decidability result can be extended beyond the ground case. We show SUP(T) is a decision procedure for the non-ground FOL fragment plus a theory T, if every non-constant function symbol from the underlying FOL signature ranges into the sort of the theory T, and every term of the theory sort is ground. Examples for T are in particular decidable fragments of arithmetic.