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.

Peirce’s triadic logic has been under discussion since its discovery in the 1960s by Fisch and Turquette. The experiments with matrices of three-valued logic are recorded in a few pages of unpublished manuscripts dated 1909, a decade before similar systems have been developed by logicians. The purposes of Peirce’s work on such logic, as well as semantical aspects of his system, are disputable. In the most extensive work about it, Turquette suggested that the matrices are related in dual pairs of (...) axiomatic Hilbert-style systems. In this paper, we present a simple tableau proof for a fragment of Peirce three-valued logic, called P3, based on similar approaches in many-valued literature. We demonstrated that this proof is sound and complete. Besides that, taking the false as the only undesignated value and adding non-classical negations to the calculus, we can explore paraconsistent and paracompleteness theories into P3. Keywords: Charles S. Peirce, many-valued logics, theory of proof, tableau method. (shrink)

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 algebraic semantics. (shrink)

Recent years have been blessed with an abundance of logical systems, arising from a multitude of applications. A logic can be characterised in many different ways. Traditionally, a logic is presented via the following three components: 1. an intuitive non-formal motivation, perhaps tie it in to some application area 2. a semantical interpretation 3. a proof theoretical formulation. There are several types of proof theoretical methodologies, Hilbert style, Gentzen style, goal directed style, labelled deductive system style, and so on. The (...) tableau methodology, invented in the 1950s by Beth and Hintikka and later per fected by Smullyan and Fitting, is today one of the most popular, since it appears to bring together the proof-theoretical and the semantical approaches to the pre of a logical system and is also very intuitive. In many universities it is sentation the style first taught to students. Recently interest in tableaux has become more widespread and a community crystallised around the subject. An annual tableaux conference is being held and proceedings are published. The present volume is a Handbook a/Tableaux pre senting to the community a wide coverage of tableaux systems for a variety of logics. It is written by active members of the community and brings the reader up to frontline research. It will be of interest to any formal logician from any area. (shrink)

In this paper we focus our attention on tableau methods for propositional interval temporal logics. These logics provide a natural framework for representing and reasoning about temporal properties in several areas of computer science. However, while various tableau methods have been developed for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based ones. We develop a general tableau method for Venema's \cdt\ logic interpreted over partial orders (...) (\nsbcdt\ for short). It combines features of the classical tableau method for first-order logic with those of explicit tableau methods for modal logics with constraint label management, and it can be easily tailored to most propositional interval temporal logics proposed in the literature. We prove its soundness and completeness, and we show how it has been implemented. (shrink)

A concept language with role intersection and number restriction is defined and its modal equivalent is provided. The main reasoning tasks of satisfiability and subsumption checking are formulated in terms of modal logic and an algorithm for their solution is provided. An axiomatization for a restricted graded modal language with intersection of modalities (the modal counterpart of the concept language we examine)is given and used in the proposed algorithm.

Adaptive logics typically pertain to reasoning procedures for which there is no positive test. In [7], we presented a tableau method for two inconsistency-adaptive logics. In the present paper, we describe these methods and present several ways to increase their efficiency. This culminates in a dynamic marking procedure that indicates which branches have to be extended first, and thus guides one towards a decision — the conclusion follows or does not follow — in a very economical way.

The propositional fragment L 1 of Leniewski's ontology is the smallest class (of formulas) containing besides all the instances of tautology the formulas of the forms: (a, b) (a, a), (a, b) (b,). (a, c) and (a, b) (b, c). (b, a) being closed under detachment. The purpose of this paper is to furnish another more constructive proof than that given earlier by one of us for: Theorem A is provable in L 1 iff TA is a thesis of first-order (...) predicate logic with equality, where T is a translation of the formulas of L 1 into those of first-order predicate logic with equality such that T(a, b) = FblxFax (Russeltian-type definite description), TA B = TA TB, T A = TA, etc. (shrink)

ABSTRACT In this paper we define two logics, KLn and BLn, and present tableau-based decision procedures for both. KLn is a temporal logic of knowledge. Thus, in addition to the usual connectives of linear discrete temporal logic, it contains a set of unary modal connectives for representing the knowledge possessed by agents. The logic BLn is somewhat similar; it is a temporal logic that contains connectives for representing the beliefs of agents. In addition to a complete formal definition of (...) the two logics and their decision procedures, the paper includes a brief review of their applications in AI and mainstream computer science, correctness proofs for the decision procedures, a number of worked examples illustrating the decision procedures, and some pointers to further work. (shrink)

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.

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 (...) problem by applying recent methods from sorted logics. This paper presents a tableau calculus that combines the proper treatment of partial functions with the efficiency of sorted calculi. (shrink)

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 the cut-rule, (...) the so-called analytical cut-rule.In addition we show that G 0is not compact (and therefore not canonical), and we proof with the tableau-method that G 0is characterised by the class of all finite, (transitive) trees of degenerate or simple clusters of worlds; therefore G 0is decidable and also characterised by the class of all frames for G 0. (shrink)

We present a dual tableau system, RLK, which is itself a deterministic decision procedure verifying validity of K-formulas. The system is constructed in the framework of the original methodology of relational proof systems, determined only by axioms and inference rules, without any external techniques. Furthermore, we describe an implementation of the system in Prolog, and we show some of its advantages.

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 (...) additional branch closure condition implementing the property that each world must be either reachable or unreachable. The calculus allows for establishing the computational complexity of reasoning about only knowing and knowing at most. Moreover, we prove that the method matches the worst-case complexity lower bound of the satisfiability problem for both ON and O. With respect to [22], in which the tableau calculus was originally presented, in this paper we both provide a formal proof of soundness and completeness of the calculus, and prove the complexity results for the logic ON. (shrink)

L'un des objectifs souvent visé par les théories esthétiques contemporaines est la compréhension de ce produit particulier de l'artiste peintre qu'est un tableau. Et, dans la recherche d'une telle compréhension, plusieurs types d'entreprises tant descriptives qu'explicatives ont déployé une diversité impressionnante de concepts et de méthodes.

O pewnym językowym rozszerzeniu logiki MR: podejście semantyczne i tabelau W artykule przedstawiamy rozszerzenie minimalnej, normalnej logiki pozycyjnej, czyli logiki z operatorem realizacji. Logika pozycyjna to logika filozoficzna, która umożliwia odniesienie zdań do kontekstów, które można rozumieć na wiele sposobów. Wzbogacamy podstawowy język minimalnej logiki pozycyjnej o dodatkowe wyrażenia zbudowane z predykatów i stałych pozycyjnych. Akceptujemy również wyrażenia zbudowane z operatorem realizacji oraz wiele pozycji, takich jak: Dzięki temu zwiększyliśmy wyrazistość minimalnej logiki pozycyjnej. W artykule wskazujemy na wiele przykładów na (...) to, że dzięki tej niewielkiej zmianie mogą powstać złożone teorie oparte na proponowanym rozszerzeniu. Jako teorię dowodu dla naszej logiki zakładamy metody tableau, pokazujące twierdzenia o poprawności i zupełności. Na koniec jednak pokazujemy, że badana tutaj logika jest tylko rozszerzeniem językowym MR: wszystkie twierdzenia o przedłużeniu mają swoje odpowiedniki w czystych twierdzeniach MR. Jednak teorie oparte na proponowanym rozszerzeniu mogą wyrazić znacznie więcej niż teorie oparte na czystej MR. (shrink)

We formulate a Hilbert-style axiomatic system and a tableau calculus for the STIT-based logic of imagination recently proposed in Wansing. Completeness of the axiom system is shown by the method of canonical models; completeness of the tableau system is also shown by using standard methods.

The semantic valuations of classical logic, strong Kleene logic, the logic of paradox and the logic of first-degree entailment, all respect the Dunn conditions: we call them Dunn logics. In this paper, we study the interpolation properties of the Dunn logics and extensions of these logics to more expressive languages. We do so by relying on the \ calculus, a signed tableau calculus whose rules mirror the Dunn conditions syntactically and which characterizes the Dunn logics in a uniform way. (...) In terms of the \ calculus, we first introduce two different interpolation methods, each of which uniformly shows that the Dunn logics have the interpolation property. One of the methods is closely related to Maehara’s method but the other method, which we call the pruned tableau method, is novel to this paper. We provide various reasons to prefer the pruned tableau method to the Maehara-style method. We then turn our attention to extensions of Dunn logics with so-called appropriate implication connectives. Although these logics have been considered at various places in the literature, a study of the interpolation properties of these logics is lacking. We use the pruned tableau method to uniformly show that these extended Dunn logics have the interpolation property and explain that the same result cannot be obtained via the Maehara-style method. Finally, we show how the pruned tableau method constructs interpolants for functionally complete extensions of the Dunn logics. (shrink)

The ancient Greek method of analysis has a rational reconstruction in the form of the tableau method of logical proof. This reconstruction shows that the format of analysis was largely determined by the requirement that proofs could be formulated by reference to geometrical figures. In problematic analysis, it has to be assumed not only that the theorem to be proved is true, but also that it is known. This means using epistemic logic, where instantiations of variables are (...) typically allowed only with respect to known objects. This requirement explains the preoccupation of Greek geometers with questions as to which geometrical objects are ?given?, that is, known or ?data?, as in the title of Euclid's eponymous book. In problematic analysis, constructions had to rely on objects that are known only hypothetically. This seems strange unless one relies on a robust idea of ?unknown? objects in the same sense as the unknowns of algebra. The Greeks did not have such a concept, which made their grasp of the analytic method shaky. (shrink)

By a pure modal logic of names we mean a quantifier-free formulation of such a logic which includes not only traditional categorical, but also modal categorical sentences with modalities de re and which is an extension of Propositional Logic. For categorical sentences we use two interpretations: a “natural” one; and Johnson and Thomason’s interpretation, which is suitable for some reconstructions of Aristotelian modal syllogistic :271–284, 1989; Thomason in J Philos Logic 22:111–128, 1993 and J Philos Logic 26:129–141, 1997. In both (...) cases we use Johnson-like models. We also analyze different kinds of versions of PMLN, for both general and singular names. We present complete tableau systems for the different versions of PMLN. These systems enable us to present some decidability methods. It yields “strong decidability” in the following sense: for every inference starting with a finite set of premises we can specify a finite number of steps to check whether it is logically valid. This method gives the upper bound of the cardinality of models needed for the examination of the validity of a given inference. (shrink)

Dix ans avant sa mort, Bernard Teyssèdre dans Arthur Rimbaud et le Foutoir zutique montre avec brio et humour comment l’enquête esthétique, historique, voire anthropologique, sur un sujet scandaleux complète celle menée à bien sur Le Roman de l’Origine (2007) et la vie du fameux tableau de Courbet, abordant avec liberté la question littéraire et celle de l’art. Mêlant avec subtilité le geste littéraire et le goût d’une recherche scientifique exigeante, sa méthode d’interprétation devient alors une œuvre d’art ouverte, (...) vertigineuse. L’exploration de son texte de 776 pages propose de repérer et de commenter la manière dont il conduit l’enquête sur Rimbaud, sur l’ Album zutique, à l’aune de divers contextes et archives. L’errance, le doute, la prudence et l’audace participent de l’immersion dans ce foutoir qui n’a pas livré tous ses secrets. (shrink)

Temporal epistemic logics are known, from results of Halpern and Vardi, to have a wide range of complexities of the satisfiability problem: from PSPACE, through non-elementary, to highly undecidable. These complexities depend on the choice of some key parameters specifying, inter alia, possible interactions between time and knowledge, such as synchrony and agents' abilities for learning and recall. In this work we develop practically implementable tableau-based decision procedures for deciding satisfiability in single-agent synchronous temporal-epistemic logics with interactions between time (...) and knowledge. We discuss some complications that occur, even in the single-agent case, when interactions between time and knowledge are assumed and show how the method of incremental tableaux can be adapted to work in EXPSPACE, respectively 2EXPTIME, for these logics, thereby also matching the upper bounds obtained for them by Halpern and Vardi. (shrink)

We present an extension of the mosaic method aimed at capturing many-dimensional modal logics. As a proof-of-concept, we define the method for logics arising from the combination of linear tense operators with an “orthogonal” S5-like modality. We show that the existence of a model for a given set of formulas is equivalent to the existence of a suitable set of partial models, called mosaics, and apply the technique not only in obtaining a proof of decidability and a proof (...) of completeness for the corresponding Hilbert-style axiomatization, but also in the development of a mosaic-based tableau system. We further consider extensions for dealing with the case when interactions between the two dimensions exist, thus covering a wide class of bundled Ockhamist branching-time logics, and present for them some partial results, such as a non-analytic version of the tableau system. (shrink)

A proof method for automation of reasoning in a paraconsistent logic, the calculus C1* of da Costa, is presented. The method is analytical, using a specially designed tableau system. Actually two tableau systems were created. A first one, with a small number of rules in order to be mathematically convenient, is used to prove the soundness and the completeness of the method. The other one, which is equivalent to the former, is a system of derived (...) rules designed to enhance computational efficiency. A prototype based on this second system was effectively implemented. (shrink)

Le Discours de la Méthode oppose explicitement « faire voir » à «enseigner». À ce propos il s'agit ici de déterminer la fonction et la signification de ces verbes dans le contexte de la communication d'un savoir. Ce Discours, plutôt que de simplement transmettre des principes généraux, veut, par le truchement du tableau d'une vie présenté sous la forme d'une « histoire » ou d'une « fable », susciter chez le lecteur l'idée correspondante de la recherche et de la (...) découverte par soi-même. Aussi, sur le plan discursif, la première catégorie verbale, au lieu d'être une attribution est une attribution différée. Ce procédé sémiotique correspond à la thèse cartésienne selon laquelle l'acquisition d'une vérité implique examen et approbation de la part du destinataire.The Discours de la Méthode explicitely opposes "to show" to "to teach". In this connection, we want here to determine the function and the meaning of these verbs in the context of the transmission of knowledge. The Discours, instead of simply conveying general principles, endeavors, through the picture of a life displayed as a "history" or "fable", to give rise to the corresponding ideas of research and discovery in the reader himself. On the discursive level, the first verbal category, far from naming the ascription of an achieved state, must be understood as the delayed attribution of that state. This semiotic procedure corresponds to the Cartesian thesis according to which the acquisition of a truth involves examination and approval on the part of the addressee. (shrink)

ABSTRACT: For the Stoics, a syllogism is a formally valid argument; the primary function of their syllogistic is to establish such formal validity. Stoic syllogistic is a system of formal logic that relies on two types of argumental rules: (i) 5 rules (the accounts of the indemonstrables) which determine whether any given argument is an indemonstrable argument, i.e. an elementary syllogism the validity of which is not in need of further demonstration; (ii) one unary and three binary argumental rules which (...) establish the formal validity of non-indemonstrable arguments by analysing them in one or more steps into one or more indemonstrable arguments (cut type rules and antilogism). The function of these rules is to reduce given non-indemonstrable arguments to indemonstrable syllogisms. Moreover, the Stoic method of deduction differs from standard modern ones in that the direction is reversed (similar to tableau methods). The Stoic system may hence be called an argumental reductive system of deduction. In this paper, a reconstruction of this system of logic is presented, and similarities to relevance logic are pointed out. (shrink)

The paper is devoted to an approach to analytic tableaux for propositional logic, but can be successfully extended to other logics. The distinguishing features of the presented approach are:(i) a precise set-theoretical description of tableau method; (ii) a notion of tableau consequence relation is defined without help of a notion of tableau, in our universe of discourse the basic notion is a branch;(iii) we define a tableau as a finite set of some chosen branches which (...) is enough to check; hence, in our approach a tableau is only a way of choosing a minimal set of closed branches;(iv) a choice of tableau can be arbitrary, it means that if one tableau starting with some set of premisses is closed in the defined sense, then every branch in the power set of the set of formulas, that starts with the same set, is closed. (shrink)

We propose a dynamic-epistemic analysis of the different epistemic operations constitutive of the process of interrogative inquiry, as described by Hintikka’s Interrogative Model of Inquiry (IMI). We develop a dynamic logic of questions for representing interrogative steps, based on Hintikka’s treatment of questions in the IMI, along with a dynamic logic of inferences for representing deductive steps, based on the tableau method. We then merge these two systems into a dynamic logic of interrogative inquiry which articulates a joint (...) treatment of questions and inferences, providing thereby a unified framework representing the informational dynamics of interrogative inquiry. We provide sound and complete axiomatic systems for the three dynamic logics that we introduce, we compare our framework with existing approaches, and we finally propose several directions for further work. (shrink)

In this paper we present tableau methods for two-dimensional modal logics. Although models for such logics are well known, proof systems remain rather unexplored as most of their developments have been purely axiomatic. The logics herein considered contain first-order quantifiers with identity, and all the formulas in the language are doubly-indexed in the proof systems, with the upper indices intuitively representing the actual or reference worlds, and the lower indices representing worlds of evaluation—first and second dimensions, respectively. The tableaux (...) modulate over different notions of validity such as local, general, and diagonal, besides being general enough for several two-dimensional logics proposed in the literature. We also motivate the introduction of a new operator into two-dimensional languages and explore some of the philosophical questions raised by it concerning the relations there are between actuality, necessity, and the a priori, that seem to undermine traditional intuitive interpretations of two-dimensional operators. (shrink)

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 into (...) account. As a consequence, the higher-order unification problem is undecidable and sets of solutions need not even always have most general elements that represent them. Thus the mentioned calculi for higher-order logic have take special measures to circumvent the problems posed by the theoretical complexity of higher-order unification. In this paper, we will exemplify the methods and proof- and model-theoretic tools needed for extending first-order automated theorem proving to higherorder logic. For the sake of simplicity take the tableau method as a basis (for a general introduction to first-order tableaux see part I.1) and discuss the higherorder tableau calculi HT and HTE first presented in [19]. The methods in this paper also apply to higher-order resolution calculi [1, 13, 6] or the higher-order matings method of Peter [3], which extend their first-order counterparts in much the same way. Since higher-order calculi cannot be complete for the standard semantics by Gödel’s incompleteness theorem [11], only the weaker notion of Henkin models [12] leads to a meaningful notion of completeness in higher-order logic. It turns out that the calculi in [1, 13, 3, 19] are not Henkin-complete, since they fail to capture the extensionality principles of higher-order logic. We will characterize the deductive power of our calculus HT (which is roughly equivalent to these calculi) by the semantics of functional Σ-models. To arrive at a calculus that is complete with respect to Henkin models, we build on ideas from [6] and augment HT with tableau construction rules that use the extensionality principles in a goal-oriented way.. (shrink)

In this paper we study proof procedures for some variants of first-order modal logics, where domains may be either cumulative or freely varying and terms may be either rigid or non-rigid, local or non-local. We define both ground and free variable tableau methods, parametric with respect to the variants of the considered logics. The treatment of each variant is equally simple and is based on the annotation of functional symbols by natural numbers, conveying some semantical information on the worlds (...) where they are meant to be interpreted.This paper is an extended version of a previous work where full proofs were not included. Proofs are in some points rather tricky and may help in understanding the reasons for some details in basic definitions. (shrink)

In this work we propose a labelled tableau method for Łukasiewicz infinite-valued logic Lω. The method is based on the Kripke semantics of this logic developed by Urquhart [25] and Scott [24]. On the one hand, our method falls under the general paradigm of labelled deduction [8] and it is rather close to the tableau systems for sub-structural logics proposed in [4]. On the other hand, it provides a CoNP decision procedure for Lω validity by (...) reducing the check of branch closure to linear programming. (shrink)

In this work we propose a labelled tableau method for ukasiewicz infinite-valued logic L . The method is based on the Kripke semantics of this logic developed by Urquhart [25] and Scott [24]. On the one hand, our method falls under the general paradigm of labelled deduction [8] and it is rather close to the tableau systems for sub-structural logics proposed in [4]. On the other hand, it provides a CoNP decision procedure for L validity (...) by reducing the check of branch closure to linear programming. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Reviewed by:The Logic Pamphlets of Charles Lutwidge Dodgson and Related PiecesIrving H. AnellisFrancine F. Abeles, editor. The Logic Pamphlets of Charles Lutwidge Dodgson and Related Pieces. The Pamphlets of Lewis Carroll, 4. New York-Charlottesville-London: Lewis Carroll Society of North America-University Press of Virginia, 2010. Pp. xx + 271. Cloth, $75.00.Until William Bartley’s rediscovery and reconstruction of Dodgson’s lost Part II of Symbolic Logic, Lewis Carroll’s reputation in logic, when (...) taken seriously, rested upon his few published articles on logical paradoxes and puzzles, while his published books, The Game of Logic and Symbolic Logic, were regarded as suitable perhaps as pedagogical tools, but dismissed otherwise as amusements, on a par with the Alice works. Richard Braithwaite asserted (“Lewis Carroll as Logician”) that “Carroll regarded formal and symbolic logic not as a corpus of systematic knowledge about valid thought nor yet as an art for teaching a person to think correctly.” He suggested that Dodgson used his pseudonym for his popular and whimsical writings, reserving his legal name only for his serious mathematical products. Philosophers practicing linguistic analysis in their assault on nonsense deriving from misuse of language meanwhile developed an interest in Carroll (e.g. George Pitcher, “Wittgenstein, Nonsense, and Lewis Carroll”). Abeles, on the contrary, stresses the seriousness of Dodgson’s pedagogical and popularizing mission (195–99).Bartley’s discovery opened the door for reevaluating Dodgson as a serious logician, and Abeles has been in the forefront of that reevaluation. Her general introduction and introductions to the main divisions of this collection of Carroll’s publications (and additional material from his Nachlass and a handful of publications of others, composed in response to Carroll’s published articles) place his serious logical work and its significance in historical perspective, providing a deeper, more sophisticated view than found in Bartley’s “Editor’s Introduction” to Lewis Carroll’s Symbolic Logic. Abeles also offers brief introductions to the individual entries, which describe their physical characteristics and circumstances of composition.Dodgson aligned with the majority of those British logicians of his day, starting with George Boole, who understood formal logic to be Aristotelian syllogistic, and symbolic logic to be syllogistic logic expressed algebraically. His notational innovation was employing indices to terms so that, independently of the arrangement of terms, propositions could easily be read; thus, “xy0” can be read as “no x are y” or “no y are x” and “x1y0” as “all x are not y” or “no x are y”. In dealing with the classical elimination problem in the class calculus—to determine the maximum information, without duplications, obtainable from a given set of premises—Dodgson in his later work and unpublished letters anticipated several concepts of automated theorem proving.Central to both geometry and to formal logic are the rules of logical inference that establish the validity of arguments and guarantee that conclusions inferred from true [End Page 506] premises are true. The modern analytic tableaux, or tree method, is a fundamental tool in this regard, both for deriving theorems and for determining the validity or invalidity of the proofs for propositional calculus and first-order predicate calculus.Introducing his reconstruction of Part II of Symbolic Logic, Bartley noted that, along with the logic diagrams that Carroll devised, he also devised a tableau method that strongly resembled Beth’s semantic tableaux. Abeles went more deeply and convincingly into that resemblance in her earlier research. Beth’s tableaux, together with Hintikka’s model sets, were the direct ancestors of Smullyan’s analytic tableaux, which in turn are the theoretical basis for the Robinson resolution method that continues to be central to much work in programming logic.Abeles has also shown that the work in Studies in Logic by Charles Peirce and his logic students at Johns Hopkins University served as a source of inspiration for Dodgson. More critically, she demonstrated that Dodgson devised and employed the tree method for carrying out proofs of syllogisms and chains of syllogisms, or soriteses, in Part II of Symbolic Logic (see her “Lewis Carroll’s Method of Trees: Its Origins in Studies in Logic,” Modern Logic 1 [1990]: 25–34). The tree... (shrink)

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, tense, relevant and other non-classical logics is connected with serious difficulties. Tableaux variants are constructed only for a few normal modal systems. As to relevant and paraconsistent logic, the absence of its tableau variants may be considered as a question of special interest. We shall formulate the tableaux for propositional modal system S4.1, S4.2, S4.3, S4.4 and relevant R∗ and E ∗ using Beth’s tableaux construction with indexed formulas. (shrink)

In this paper we integrate a sorted unification calculus into free variable tableau methods for logics with term declarations. The calculus we define is used to close a tableau at once, unifying a set of equations derived from pairs of potentially complementary literals occurring in its branches. Apart from making the deduction system sound and complete, the calculus is terminating and so, it can be used as a decision procedure. In this sense we have separated the complexity of (...) sorts from the undecidability of first order logic. (shrink)

Normative arrow update logic (NAUL) is a logic that combines normative temporal logic (NTL) and arrow update logic (AUL). In NAUL, norms are interpreted as arrow updates on labeled transition systems with a CTL-like logic. We show that the satisfiability problem of NAUL is decidable with a tableau method and it is in EXPSPACE.

In this paper we describe an improvement of Smullyan's analytic tableau method for the propositional calculus-Improved Parent Clash Restricted (IPCR) tableau-and show that it is equivalent to SL-resolution in complexity.