Results for 'tableau calculi'

927 found
Order:
  1.  87
    Connection tableau calculi with disjunctive constraints.Ortrun Ibens - 2002 - Studia Logica 70 (2):241 - 270.
    Automated theorem proving amounts to solving search problems in usually tremendous search spaces. A lot of research therefore focuses on search space reductions. Our approach reduces the search space which arises when using so-called connection tableau calculi for first-order automated theorem proving. It uses disjunctive constraints over first-order equations to compress certain parts of this search space. We present the basics of our constrained-connection-tableau calculi, a constraint extension of connection tableau calculi, and deal with (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  2.  20
    Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics.A. Avellone, M. Ferrari & P. Miglioli - 1999 - Logic Journal of the IGPL 7 (4):447-480.
    We get cut-free sequent calculi for the interpolable propositional intermediate logics by translating suitable duplication-free tableau calculi developed within a semantical framework. From this point of view, the paper also provides semantical proofs of the admissibility of the cut-rule for appropriate cut-free sequent calculi.
    Direct download  
     
    Export citation  
     
    Bookmark   8 citations  
  3.  52
    Modal tableau calculi and interpolation.Wolfgang Rautenberg - 1983 - Journal of Philosophical Logic 12 (4):403 - 423.
  4.  33
    Labelled tableau calculi for weak modal logics.Andrzej Indrzejczak - 2007 - Bulletin of the Section of Logic 36 (3-4):159-173.
  5.  77
    Cut-free tableau calculi for some propositional normal modal logics.Martin Amerbauer - 1996 - Studia Logica 57 (2-3):359 - 372.
    We give sound and complete tableau and sequent calculi for the prepositional normal modal logics S4.04, K4B and G 0(these logics are the smallest normal modal logics containing K and the schemata A A, A A and A ( A); A A and AA; A A and ((A A) A) A resp.) with the following properties: the calculi for S4.04 and G 0are cut-free and have the interpolation property, the calculus for K4B contains a restricted version of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  6.  59
    Cut-free tableau calculi for some intuitionistic modal logics.Mauro Ferrari - 1997 - Studia Logica 59 (3):303-330.
    In this paper we provide cut-free tableau calculi for the intuitionistic modal logics IK, ID, IT, i.e. the intuitionistic analogues of the classical modal systems K, D and T. Further, we analyse the necessity of duplicating formulas to which rules are applied. In order to develop these calculi we extend to the modal case some ideas presented by Miglioli, Moscato and Ornaghi for intuitionistic logic. Specifically, we enlarge the language with the new signs Fc and CR near (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  7.  13
    New Tableau Characterizations for Non-clausal MaxSAT Problem.Guido Fiorino - 2022 - Logic Journal of the IGPL 30 (3):422-436.
    In this paper, we provide non-clausal tableau calculi for the maximum satisfiability problem and its variants. We discuss both basic calculi to characterize the problem and their modifications to reduce the proof size.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  8.  56
    ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse.Linh Anh Nguyen & Andrzej Szałas - 2011 - Studia Logica 98 (3):387-428.
    Grammar logics were introduced by Fariñas del Cerro and Penttonen in 1988 and have been widely studied. In this paper we consider regular grammar logics with converse ( REG c logics) and present sound and complete tableau calculi for the general satisfiability problem of REG c logics and the problem of checking consistency of an ABox w.r.t. a TBox in a REG c logic. Using our calculi we develop ExpTime (optimal) tableau decision procedures for the mentioned (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  9. A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications.Mauro Ferrari, Camillo Fiorentini & Guido Fiorino - 2009 - Journal of Applied Non-Classical Logics 19 (2):149-166.
    Since 1993, when Hudelmaier developed an O(n log n)-space decision procedure for propositional Intuitionistic Logic, a lot of work has been done to improve the efficiency of the related proof-search algorithms. In this paper a tableau calculus using the signs T, F and Fc with a new set of rules to treat signed formulas of the kind T((A → B) → C) is provided. The main feature of the calculus is the reduction of both the non-determinism in proof-search and (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  10.  31
    Tableau Systems for Deontic Action Logics Based on Finite Boolean Algebras, and Their Complexity.Pablo F. Castro - 2017 - Studia Logica 105 (2):229-251.
    We introduce a family of tableau calculi for deontic action logics based on finite boolean algebras, these logics provide deontic operators which are applied to a finite number of actions ; furthermore, in these formalisms, actions can be combined by means of boolean operators, this provides an expressive algebra of actions. We define a tableau calculus for the basic logic and then we extend this calculus to cope with extant variations of this formalism; we prove the soundness (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  11.  89
    A sound and complete tableau calculus for reasoning about only knowing and knowing at most.Riccardo Rosati - 2001 - Studia Logica 69 (1):171-191.
    We define a tableau calculus for the logic of only knowing and knowing at most ON, which is an extension of Levesque's logic of only knowing O. The method is based on the possible-world semantics of the logic ON, and can be considered as an extension of known tableau calculi for modal logic K45. From the technical viewpoint, the main features of such an extension are the explicit representation of "unreachable" worlds in the tableau, and an (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  12.  47
    Labeled sequent calculi for modal logics and implicit contractions.Pierluigi Minari - 2013 - Archive for Mathematical Logic 52 (7-8):881-907.
    The paper settles an open question concerning Negri-style labeled sequent calculi for modal logics and also, indirectly, other proof systems which make (more or less) explicit use of semantic parameters in the syntax and are thus subsumed by labeled calculi, like Brünnler’s deep sequent calculi, Poggiolesi’s tree-hypersequent calculi and Fitting’s prefixed tableau systems. Specifically, the main result we prove (through a semantic argument) is that labeled calculi for the modal logics K and D remain (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  13. A tableau calculus for partial functions.Manfred Kerber Michael Kohlhase - unknown
    Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using a three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truthfunctional, does not fit the framework directly. We solve this (...)
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  14.  68
    Decision procedures for some strong hybrid logics.Andrzej Indrzejczak & Michał Zawidzki - 2013 - Logic and Logical Philosophy 22 (4):389-409.
    Hybrid logics are extensions of standard modal logics, which significantly increase the expressive power of the latter. Since most of hybrid logics are known to be decidable, decision procedures for them is a widely investigated field of research. So far, several tableau calculi for hybrid logics have been presented in the literature. In this paper we introduce a sound, complete and terminating tableau calculus T H(@,E,D, ♦ −) for hybrid logics with the satisfaction operators, the universal modality, (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  15. Analytic Tableaux for all of SIXTEEN 3.Stefan Wintein & Reinhard Muskens - 2015 - Journal of Philosophical Logic 44 (5):473-487.
    In this paper we give an analytic tableau calculus P L 1 6 for a functionally complete extension of Shramko and Wansing’s logic. The calculus is based on signed formulas and a single set of tableau rules is involved in axiomatising each of the four entailment relations ⊧ t, ⊧ f, ⊧ i, and ⊧ under consideration—the differences only residing in initial assignments of signs to formulas. Proving that two sets of formulas are in one of the first (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  16.  58
    Connexive Conditional Logic. Part I.Heinrich Wansing & Matthias Unterhuber - 2019 - Logic and Logical Philosophy 28 (3):567-610.
    In this paper, first some propositional conditional logics based on Belnap and Dunn’s useful four-valued logic of first-degree entailment are introduced semantically, which are then turned into systems of weakly and unrestrictedly connexive conditional logic. The general frame semantics for these logics makes use of a set of allowable (or admissible) extension/antiextension pairs. Next, sound and complete tableau calculi for these logics are presented. Moreover, an expansion of the basic conditional connexive logics by a constructive implication is considered, (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  17.  65
    Modal logics with Belnapian truth values.Serge P. Odintsov & Heinrich Wansing - 2010 - Journal of Applied Non-Classical Logics 20 (3):279-304.
    Various four- and three-valued modal propositional logics are studied. The basic systems are modal extensions BK and BS4 of Belnap and Dunn's four-valued logic of firstdegree entailment. Three-valued extensions of BK and BS4 are considered as well. These logics are introduced semantically by means of relational models with two distinct evaluation relations, one for verification and the other for falsification. Axiom systems are defined and shown to be sound and complete with respect to the relational semantics and with respect to (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   33 citations  
  18.  29
    Deductive Systems and the Decidability Problem for Hybrid Logics.Michał Zawidzki - 2014 - Cambridge University Press.
    This book stands at the intersection of two topics: the decidability and computational complexity of hybrid logics, and the deductive systems designed for them. Hybrid logics are here divided into two groups: standard hybrid logics involving nominals as expressions of a separate sort, and non-standard hybrid logics, which do not involve nominals but whose expressive power matches the expressive power of binder-free standard hybrid logics.The original results of this book are split into two parts. This division reflects the division of (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  19. Tractarian First-Order Logic: Identity and the N-Operator.Brian Rogers & Kai F. Wehmeier - 2012 - Review of Symbolic Logic 5 (4):538-573.
    In theTractatus, Wittgenstein advocates two major notational innovations in logic. First, identity is to be expressed by identity of the sign only, not by a sign for identity. Secondly, only one logical operator, called “N” by Wittgenstein, should be employed in the construction of compound formulas. We show that, despite claims to the contrary in the literature, both of these proposals can be realized, severally and jointly, in expressively complete systems of first-order logic. Building on early work of Hintikka’s, we (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  20.  23
    Connexive Variants of Modal Logics Over FDE.Sergei Odintsov, Daniel Skurt & Heinrich Wansing - 2021 - In Ofer Arieli & Anna Zamansky, Arnon Avron on Semantics and Proof Theory of Non-Classical Logics. Springer Verlag. pp. 295-318.
    Various connexive FDE-based modal logics are studied. Some of these logics contain a conditional that is both connexive and strict, thereby highlighting that strictness and connexivity of a conditional do not exclude each other. In particular, the connexive modal logics cBK-\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$^{-}$$\end{document}, cKN4, scBK-\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$^{-}$$\end{document}, scKN4, cMBL, and scMBL are introduced semantically by means of classes of Kripke models. The logics cBK-\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} (...)
    Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  21. Non-Analytic Tableaux for Chellas's Conditional Logic CK and Lewis's Logic of Counterfactuals VC.Richard Zach - 2018 - Australasian Journal of Logic 15 (3):609-628.
    Priest has provided a simple tableau calculus for Chellas's conditional logic Ck. We provide rules which, when added to Priest's system, result in tableau calculi for Chellas's CK and Lewis's VC. Completeness of these tableaux, however, relies on the cut rule.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  22.  72
    De Finettian Logics of Indicative Conditionals Part II: Proof Theory and Algebraic Semantics.Paul Égré, Lorenzo Rossi & Jan Sprenger - 2021 - Journal of Philosophical Logic 50 (2):215-247.
    In Part I of this paper, we identified and compared various schemes for trivalent truth conditions for indicative conditionals, most notably the proposals by de Finetti and Reichenbach on the one hand, and by Cooper and Cantwell on the other. Here we provide the proof theory for the resulting logics DF/TT and CC/TT, using tableau calculi and sequent calculi, and proving soundness and completeness results. Then we turn to the algebraic semantics, where both logics have substantive limitations: (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  23. Higher-order automated theorem proving.Michael Kohlhase - unknown
    The history of building automated theorem provers for higher-order logic is almost as old as the field of deduction systems itself. The first successful attempts to mechanize and implement higher-order logic were those of Huet [13] and Jensen and Pietrzykowski [17]. They combine the resolution principle for higher-order logic (first studied in [1]) with higher-order unification. The unification problem in typed λ-calculi is much more complex than that for first-order terms, since it has to take the theory of αβη-equality (...)
     
    Export citation  
     
    Bookmark   5 citations  
  24. Advances in Modal Logic, Volume.F. Wolter, H. Wansing, M. de Rijke & M. Zakharyaschev - unknown
    We study a propositional bimodal logic consisting of two S4 modalities £ and [a], together with the interaction axiom scheme a £ϕ → £ aϕ. In the intended semantics, the plain £ is given the McKinsey-Tarski interpretation as the interior operator of a topology, while the labelled [a] is given the standard Kripke semantics using a reflexive and transitive binary relation a. The interaction axiom expresses the property that the Ra relation is lower semi-continuous with respect to the topology. The (...)
     
    Export citation  
     
    Bookmark   2 citations  
  25. System description: The tableaux work bench.Rajeev Gore - manuscript
    The Tableaux Work Bench (TWB) is a meta tableau system designed for logicians with limited programming or automatic reasoning knowledge to experiment with new tableau calculi and new decision procedures. It has a simple interface, a history mechanism for controlling loops or pruning the search space, and modal simplification.
     
    Export citation  
     
    Bookmark   1 citation  
  26.  36
    Nelson's paraconsistent logics.Seiki Akama - 1999 - Logic and Logical Philosophy 7:101.
    David Nelson’s constructive logics with strong negation may beviewed as alternative paraconsistent logic. These logics have been developedbefore da Costa’s works. We address some philosophical aspects of Nelson’slogics and give technical results concerning Kripke models and tableau calculi. We also suggest possible applications of paraconsistent constructivelogics.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  27.  66
    Two Decision Procedures for da Costa’s $$C_n$$ C n Logics Based on Restricted Nmatrix Semantics.Marcelo E. Coniglio & Guilherme V. Toledo - 2022 - Studia Logica 110 (3):601-642.
    Despite being fairly powerful, finite non-deterministic matrices are unable to characterize some logics of formal inconsistency, such as those found between mbCcl and Cila. In order to overcome this limitation, we propose here restricted non-deterministic matrices (in short, RNmatrices), which are non-deterministic algebras together with a subset of the set of valuations. This allows us to characterize not only mbCcl and Cila (which is equivalent, up to language, to da Costa's logic C_1) but the whole hierarchy of da Costa's (...) C_n. This produces a novel decision procedure for these logics. Moreover, we show that the RNmatrix semantics proposed here induces naturally a labelled tableau system for each C_n, which constitutes another decision procedure for these logics. This new semantics allows us to conceive da Costa's hierarchy of C-systems as a family of (non deterministically) (n+2)-valued logics, where n is the number of "inconsistently true" truth-values and 2 is the number of "classical" or "consistent" truth-values, for every C_n. (shrink)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  28.  34
    Foundations of a theorem prover for functional and mathematical uses.Javier Leach & Susana Nieva - 1993 - Journal of Applied Non-Classical Logics 3 (1):7-38.
    ABSTRACT A computational logic, PLPR (Predicate Logic using Polymorphism and Recursion) is presented. Actually this logic is the object language of an automated deduction system designed as a tool for proving mathematical theorems as well as specify and verify properties of functional programs. A useful denotationl semantics and two general deduction methods for PLPR are defined. The first one is a tableau algorithm proved to be complete and also used as a guideline for building complete calculi. The second (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  29.  21
    Tableaux variants of some modal and relevant systems.P. I. Bystrov - 1988 - Bulletin of the Section of Logic 17 (3/4):92-98.
    The tableaux-constructions have a number of properties which advantageously distinguish them from equivalent axiomatic systems . The proofs in the form of tableaux-constructions have a full accordance with semantic interpretation and subformula property in the sense of Gentzen’s Hauptsatz. Method of tatleaux-construction gives a good substitute of Gentzen’s methods and thus opens a good perspective for the investigations of theoretical as well as applied aspects of logical calculi. It should be noted that application of tableau method in modal, (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  30. Prefixed tableaus and nested sequents.Melvin Fitting - 2012 - Annals of Pure and Applied Logic 163 (3):291 - 313.
    Nested sequent systems for modal logics are a relatively recent development, within the general area known as deep reasoning. The idea of deep reasoning is to create systems within which one operates at lower levels in formulas than just those involving the main connective or operator. Prefixed tableaus go back to 1972, and are modal tableau systems with extra machinery to represent accessibility in a purely syntactic way. We show that modal nested sequents and prefixed modal tableaus are notational (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   21 citations  
  31. Dual Systems of Sequents and Tableaux for Many-Valued Logics.Matthias Baaz, Christian G. Fermüller & Richard Zach - 1993 - Bulletin of the EATCS 51:192-197.
    The aim of this paper is to emphasize the fact that for all finitely-many-valued logics there is a completely systematic relation between sequent calculi and tableau systems. More importantly, we show that for both of these systems there are al- ways two dual proof sytems (not just only two ways to interpret the calculi). This phenomenon may easily escape one’s attention since in the classical (two-valued) case the two systems coincide. (In two-valued logic the assignment of a (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  32.  2
    Tautology Elimination, Cut Elimination, and S5.Andrzej Indrzejczak - 2017 - Logic and Logical Philosophy 26 (4):461-471.
    Tautology elimination rule was successfully applied in automated deduction and recently considered in the framework of sequent calculi where it is provably equivalent to cut rule. In this paper we focus on the advantages of proving admissibility of tautology elimination rule instead of cut for sequent calculi. It seems that one may find simpler proofs of admissibility for tautology elimination than for cut admissibility. Moreover, one may prove its admissibility for some calculi where constructive proofs of cut (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  33.  86
    Commodious axiomatization of quantifiers in multiple-valued logic.Reiner Hähnle - 1998 - Studia Logica 61 (1):101-121.
    We provide tools for a concise axiomatization of a broad class of quantifiers in many-valued logic, so-called distribution quantifiers. Although sound and complete axiomatizations for such quantifiers exist, their size renders them virtually useless for practical purposes. We show that for quantifiers based on finite distributive lattices compact axiomatizations can be obtained schematically. This is achieved by providing a link between skolemized signed formulas and filters/ideals in Boolean set lattices. Then lattice theoretic tools such as Birkhoff's representation theorem for finite (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  34.  77
    Admissibility of cut in congruent modal logics.Andrzej Indrzejczak - 2011 - Logic and Logical Philosophy 20 (3):189-203.
    We present a detailed proof of the admissibility of cut in sequent calculus for some congruent modal logics. The result was announced much earlier during the Trends in Logic Conference, Toruń 2006 and the proof for monotonic modal logics was provided already in Indrzejczak [5]. Also some tableau and natural deduction formalizations presented in Indrzejczak [6] and Indrzejczak [7] were based on this result but the proof itself was not published so far. In this paper we are going to (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  35.  10
    Szabolcs Mikulas.Gabbay-Style Calculi - 1996 - In Heinrich Wansing, Proof theory of modal logic. Boston: Kluwer Academic Publishers. pp. 243.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  36. François Lepage, Elias Thijsse, Heinrich Wansing/In-troduction 1 J. Michael Dunn/Partiality and its Dual 5 Jan van Eijck/Making Things Happen 41 William M. Farmer, Joshua D. Guttman/A Set Theory. [REVIEW]René Lavendhomme, Thierry Lucas & Sequent Calculi - 2000 - Studia Logica 66:447-448.
  37.  55
    Hypersequent Calculi for S5: The Methods of Cut Elimination.Kaja Bednarska & Andrzej Indrzejczak - 2015 - Logic and Logical Philosophy 24 (3):277–311.
    S5 is one of the most important modal logic with nice syntactic, semantic and algebraic properties. In spite of that, a successful (i.e. cut-free) formalization of S5 on the ground of standard sequent calculus (SC) was problematic and led to the invention of numerous nonstandard, generalized forms of SC. One of the most interesting framework which was very often used for this aim is that of hypersequent calculi (HC). The paper is a survey of HC for S5 proposed by (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  38. Proof tableau formulations of some first-order relevant ortho-logics.Michael Mcrobbie & Nuel Belnap Jr - 1984 - Bulletin of the Section of Logic 13 (4):233-239.
    In [6] proof tableau formulations were given of the implication/negation fragments of the important zero-order relevant logics E and R and the semirelevant logic RM . The main purpose of this paper then, is to extend results by giving proof tableau formulations of the distribution-free fragments of E, R and RM and of their first order extensions EQ, RQ and RMQ. Where X is one of these logics, we shall follow [13] in calling its distribution-free fragment OX – (...)
     
    Export citation  
     
    Bookmark   1 citation  
  39. Analytic Calculi for Circular Concepts by Finite Revision.Riccardo Bruni - 2013 - Studia Logica 101 (5):915-932.
    The paper introduces Hilbert– and Gentzen-style calculi which correspond to systems ${\mathsf{C}_{n}}$ from Gupta and Belnap [3]. Systems ${\mathsf{C}_{n}}$ were shown to be sound and complete with respect to the semantics of finite revision. Here, it is shown that Gentzen-style systems ${\mathsf{GC}_{n}}$ admit a syntactic proof of cut elimination. As a consequence, it follows that they are consistent.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  40.  7
    Tableau naturel des rapports qui existent entre Dieu, l'homme et l'univers.Louis-Claude de Saint-Martin - 1974 - Paris,: R. Dumas.
    Le Tableau naturel des rapports qui existent entre Dieu, l'homme et l'univers est un ouvrage fondamental pour ceux qui cherchent à comprendre les mystères de la Création. Pour Louis-Claude de Saint-Martin, l'homme porte en lui-même la clé de tous les mystères. Se connaître soi-même est donc la condition primordiale pour accéder à la Connaissance. Les textes sacrés nous enseignent que l'histoire de l'humanité est liée à un drame en trois actes. Le premier est celui de l'âge d'or ; le (...)
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  41.  26
    Labelled Tableau Systems for Some Subintuitionistic Logics.Minghui Ma - 2019 - Logica Universalis 13 (2):273-288.
    Labelled tableau systems are developed for subintuitionistic logics \, \ and \. These subintuitionistic logics are embedded into corresponding normal modal logics. Hintikka’s model systems are applied to prove the completeness of labelled tableau systems. The finite model property, decidability and disjunction property are obtained by labelled tableau method.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  42. Semantic tableau versions of some normal modal systems with propositional quantifiers.Daniel Rönnedal - 2019 - Organon F: Medzinárodný Časopis Pre Analytickú Filozofiu 47 (4):505–536.
    In Symbolic Logic (1932), C. I. Lewis developed five modal systems S1 − S5. S4 and S5 are so-called normal modal systems. Since Lewis and Langford’s pioneering work many other systems of this kind have been investigated, among them the 32 systems that can be generated by the five axioms T, D, B, 4 and 5. Lewis also discusses how his systems can be augmented by propositional quantifiers and how these augmented logics allow us to express some interesting ideas that (...)
     
    Export citation  
     
    Bookmark   1 citation  
  43.  58
    Epsilon calculi.Hartley Slater - 2001 - Internet Encyclopedia of Philosophy.
    Epsilon Calculi are extended forms of the predicate calculus that incorporate epsilon terms. Epsilon terms are individual terms of the form ‘εxFx’, being defined for all predicates in the language. The epsilon term ‘εxFx’ denotes a chosen F, if there are any F’s, and has an arbitrary reference otherwise. Epsilon calculi were originally developed to study certain forms of Arithmetic, and Set Theory; also to prove some important meta-theorems about the predicate calculus. Later formal developments have included a (...)
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  44.  28
    Sequent Calculi for Orthologic with Strict Implication.Tomoaki Kawano - 2022 - Bulletin of the Section of Logic 51 (1):73-89.
    In this study, new sequent calculi for a minimal quantum logic ) are discussed that involve an implication. The sequent calculus \ for \ was established by Nishimura, and it is complete with respect to ortho-models. As \ does not contain implications, this study adopts the strict implication and constructs two new sequent calculi \ and \ as the expansions of \. Both \ and \ are complete with respect to the O-models. In this study, the completeness and (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  45.  61
    Terminating tableau systems for hybrid logic with difference and converse.Mark Kaminski & Gert Smolka - 2009 - Journal of Logic, Language and Information 18 (4):437-464.
    This paper contributes to the principled construction of tableau-based decision procedures for hybrid logic with global, difference, and converse modalities. We also consider reflexive and transitive relations. For converse-free formulas we present a terminating control that does not rely on the usual chain-based blocking scheme. Our tableau systems are based on a new model existence theorem.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  46.  19
    Lambda Calculi: A Guide for the Perplexed.Chris Hankin - 1994 - Oxford University Press.
    The lambda-calculus lies at the very foundation of computer science. Besides its historical role in computability theory it has had significant influence on programming language design and implementation, denotational semantics and domain theory. The book emphasizes the proof theory for the type-free lambda-calculus. The first six chapters concern this calculus and cover the basic theory, reduction, models, computability, and the relationship between the lambda-calculus and combinatory logic. Chapter 7 presents a variety of typed calculi; first the simply typed lambda-calculus, (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  47.  34
    Hypersequent calculi for intuitionistic logic with classical atoms.Hidenori Kurokawa - 2010 - Annals of Pure and Applied Logic 161 (3):427-446.
    We discuss a propositional logic which combines classical reasoning with constructive reasoning, i.e., intuitionistic logic augmented with a class of propositional variables for which we postulate the decidability property. We call it intuitionistic logic with classical atoms. We introduce two hypersequent calculi for this logic. Our main results presented here are cut-elimination with the subformula property for the calculi. As corollaries, we show decidability, an extended form of the disjunction property, the existence of embedding into an intuitionistic modal (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  48.  35
    The Tableau Method for a Logical System Based on a Finite Poset.Abir Nour - 2002 - Journal of Applied Non-Classical Logics 12 (1):43-62.
    In order to modelize the reasoning of intelligent agents represented by a poset T, H. Rasiowa introduced logic systems called “Approximation Logics”. In these systems a set of constants constitutes a fundamental tool. In this paper, we consider logic systems called L'T without this kind of constants but limited to the case where T is a finite poset. We study the tableau method for this system and we prove its completeness for a class of formulas with respect to an (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  49.  74
    Analytic Calculi for Product Logics.George Metcalfe, Nicola Olivetti & Dov Gabbay - 2004 - Archive for Mathematical Logic 43 (7):859-889.
    Product logic Π is an important t-norm based fuzzy logic with conjunction interpreted as multiplication on the real unit interval [0,1], while Cancellative hoop logic CHL is a related logic with connectives interpreted as for Π but on the real unit interval with 0 removed (0,1]. Here we present several analytic proof systems for Π and CHL, including hypersequent calculi, co-NP labelled calculi and sequent calculi.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  50.  15
    Tableau methods for propositional logic and term logic.Tomasz Jarmużek - 2020 - Berlin: Peter Lang. Edited by Sławomir Jaskóloski & Jan Hartman.
    The book aims to formalise tableau methods for the logics of propositions and names. The methods described are based on Set Theory. The tableau rule was reduced to an ordered n-tuple of sets of expressions where the first element is a set of premises, and the following elements are its supersets.
    Direct download  
     
    Export citation  
     
    Bookmark  
1 — 50 / 927