We offer tableaux systems for logics of essence and accident and logics of non-contingency, showing their soundness and completeness for Kripke semantics. We also show an interesting parallel between these logics based on the semantic insensitivity of the two non-normal operators by which these logics are expressed.

We show that Smullyan's analytic tableaux cannot p-simulate the truth-tables. We identify the cause of this computational breakdown and relate it to an underlying semantic difficulty which is common to the whole tradition originating in Gentzen's sequent calculus, namely the dissonance between cut-free proofs and the Principle of Bivalence. Finally we discuss some ways in which this principle can be built into a tableau-like method without affecting its analytic nature.

El sistema de demostración KE es una variante de los tableaux analíticos pero es computacionalmente más eficiente que estos. Este sistema fue extendido a la lógica intuicionista proposicional recientemente. Además de su eficiencia y a diferencia de los resolvedores SAT, el sistema KE intuicionista no requiere transformaciones a formas normales y es modular en tanto que se puede extender, simple y naturalmente, a una familia amplia de lógicas que admiten semánticas relacionales. En este trabajo exploramos parte de esta modularidad, (...) extendiendo KE a una familia de lógicas modales intuicionistas, las cuales tienen aplicaciones relevantes en razonamiento automatizado y verificación formal. (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)

We show how to correct the analytic tableaux system from the paper Olkhovikov and Wansing, 259–279, 2018).

The book presents logical foundations of dual tableaux together with a number of their applications both to logics traditionally dealt with in mathematics and philosophy (such as modal, intuitionistic, relevant, and many-valued logics) and to various applied theories of computational logic (such as temporal reasoning, spatial reasoning, fuzzy-set-based reasoning, rough-set-based reasoning, order-of magnitude reasoning, reasoning about programs, threshold logics, logics of conditional decisions). The distinguishing feature of most of these applications is that the corresponding dual tableaux are built (...) in a relational language which provides useful means of presentation of the theories. In this way modularity of dual tableaux is ensured. We do not need to develop and implement each dual tableau from scratch, we should only extend the relational core common to many theories with the rules specific for a particular theory. (shrink)

The aim of this work is to introduce a series of requisites for building sound and complete tableaux systems for inferential logics based on non-deterministic valuation schemes and extend them with rules for metainferences, thus yielding metainferential tableaux system capable of proving metainferences of any level n. We show the construction of our tableaux for the logics of the Strong Kleene family and a wide range of different logical systems, most of which have not been studied previously (...) from a metainferential standpoint. Furthermore, we implement this system into a user-friendly, publicly accessible software, designed both for educational purposes as well as assistance in research endeavors. (shrink)

In this dissertation we present proof systems for several modal logics. These proof systems are based on analytic (or semantic) tableaux. Modal logics are logics for reasoning about possibility, knowledge, beliefs, preferences, and other modalities. Their semantics are almost always based on Saul Kripke’s possible world semantics. In Kripke semantics, models are represented by relational structures or, equivalently, labeled graphs. Syntactic formulas that express statements about knowledge and other modalities are evaluated in terms of such models. This dissertation focuses (...) on modal logics with dynamic operators for public announcements, belief revision, preference upgrades, and so on. These operators are defined in terms of mathematical operations on Kripke models. Thus, for example, a belief revision operator in the syntax would correspond to a belief revision operation on models. The ‘dynamic’ semantics of dynamic modal logics are a clever way of extending languages without compromising on intuitiveness. We present ‘dynamic’ tableau proof systems for these dynamic semantics, with the express aim to make them conceptually simple, easy to use, modular, and extensible. This we do by reflecting the semantics as closely as possible in the components of our tableau system. For instance, dynamic operations on Kripke models have counterpart dynamic relations between tableaux. Soundness, completeness, and decidability are three of the most important properties that a proof system may have. A proof system is sound if and only if any formula for which a proof exists, is true in every model. A proof system is complete if and only if for any formula that is true in all models, a proof exists. A proof system is decidable if and only if any formula can be proved to be a theorem or not a theorem in a finite number of steps. All proof systems in this dissertation are sound, complete, and decidable. Part of our strategy to create modular tableau systems is to delay concerns over decidability until after soundness and completeness have been established. Decidability is attained through the operations of folding and through operations on ‘tableau cascades’, which are graphs of tableaux. Finally, we provide a proof-of-concept implementation of our dynamic tableau system for public announcement logic in the Clojure programming language. (shrink)

The paper describes tableaux based proof methods for temporal logics of knowledge allowing non-trivial interaction axioms between the modal and temporal components, namely those of synchrony and no learning and synchrony and perfect recall. The interaction axioms allow the description of how knowledge evolves over time and makes reasoning in such logics theoretically more complex. Such logics can be used to specify systems that involve the knowledge of processes or agents and which change over time, for example agent based (...) systems, knowledge games or security protocols. Soundness, completeness and termination results for the tableaux are proved. (shrink)

ABSTRACT Extending a previous approach devoted to Reiter's default logic, this paper defines a general tableaux-based framework for the computation of extensions for several well-know default logics. The ideas are (1) to qualify the differences between the variant under consideration inside a single process that can switch easily from one variants to another, (2) to relate the construction of a tractable tableau representation of extensions to the idea of compiling default theories.

Motivated by H. Curry’s well-known objection and by a proposal of L. Henkin, this article introduces the positive tableaux, a form of tableau calculus without refutation based upon the idea of implicational triviality. The completeness of the method is proven, which establishes a new decision procedure for the (classical) positive propositional logic. We also introduce the concept of paratriviality in order to contribute to the question of paradoxes and limitations imposed by the behavior of classical implication.

In this paper we present a new hierarchy of analytical tableaux systems TNDC n, 1≤ntableaux formulation, we introduce da Costa's?ball? operator?o?, the generalized operators?k? and?(k)?, for 1≤k, and the negations?~k?, for k≥1, as primitive operators, differently to what has been done in the literature, where these operators are usually defined operators. We prove a version of Cut Rule for the TNDC n, 1≤n (...) that these systems are logically equivalent to the corresponding systems Cn, 1≤nshrink)

In the paper, we examine tableau systems for R. Epstein’s logics of content relationship: D (Dependence Logic), DD (Dual Dependence Logic), Eq (Logic of Equality of Content), S (Symmetric Relatedness Logic) and R (Nonsymmetric Relatedness Logic) (cf. Epstein in Philos Stud 36:137–173, 1979, Epstein in Rep. Math. Logic 21:19–34, 1987, Klonowski in Logic Log Philos 30(4):579–629, 2021, Krajewski in J Non Class Logic 8:7–33, 1991). The first tableau systems for those logics were defined by Carnielli. However, his approach has some (...) limitations, for example, it requires a proof of functional completeness and axiomatization. Notwithstanding the first two constraints, it does not include all Epstein logics, e.g., logic Eq. Unlike Carnielli’s approach, here we use set-assignment semantics to determine those logics. Since syntax and semantics of a given logic usually determine a minimal syntax and structure of a tableau system for the logic along with other properties, we propose a uniform tableau framework for the logics determined by set-assignment semantics. What distinguishes our tableau systems is that they combine the features of tableaux for propositional logics and syllogistic logics when the problem of content of propositions is analysed in tableau proofs. To denote the content of propositions in the proofs, we use generalised labels (see Jarmużek and Goré in Landscapes in Logic, College Publications, London, 2021). (shrink)

Wittgensteinian predicate logic (W-logic) is characterized by the requirement that the objects mentioned within the scope of a quantifier be excluded from the range of the associated bound variable. I present a sound and complete tableaux calculus for this logic and discuss issues of translatability between Wittgensteinian and standard predicate logic in languages with and without individual constants. A metalinguistic co-denotation predicate, akin to Frege’s triple bar of the Begriffsschrift, is introduced and used to bestow the full expressive power (...) of first-order logic with identity on W-logic in the presence of constants. (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 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 three entailment (...) relations will in general require developing four tableaux, while proving that they are in the ⊧ relation may require six. (shrink)

In this paper synthetic tableaux for Łukasiewicz's calculus Ł3 are presented in detail. Basic properties of synthetic tableaux are described as well as a systematic procedure for constructing a tableau for any given formula of Ł3. © 2011 Elsevier B.V., All rights reserved.

The forward convergence constraint is important to time analysis. Without it, given two future moments to the same point, the time branches. This is unacceptable if one assumes that time is linear. Nevertheless, one may wish to consider time-branching in order to discuss future possibilities. One can have both a linear order for the time and branching through the combination of the tense logic semantics with those of an alethic logic which allows the evaluation of the timelines of other possible (...) worlds. In this paper, I give the semantics and the tableaux systems for some alethic-tense logics. I review one in which worlds differ on their time orders, another in which they agree on the time order, a pair of conditional tense logics ), and the first-order version of MT. A brief philosophical discussion arises from every system. (shrink)

This is the first paper on constructive concurrent dynamic logic . For the first time, either for concurrent or sequential dynamic logic, we give a satisfactory treatment of what statements are forced to be true by partial information about the underlying computer. Dynamic logic was developed by Pratt [V. Pratt, Semantical considerations on Floyd–Hoare logic, in: 17th Annual IEEE Symp. on Found. Comp. Sci., New York, 1976, pp. 109–121, V. Pratt, Applications of modal logic to programming, Studia Logica 39 257–274] (...) for nondeterministic sequential programs, and by Peleg [D. Peleg, Concurrent dynamic logic, Journal of the Association for Computing Machinery 34 , D. Peleg, Communication in concurrent dynamic logic, Journal of Computer and System Sciences 35 ] for concurrent programs, for the purpose of proving properties of programs such as correctness. Here we define what it means for a dynamic logic formula to be forced to be true knowing only partial information about the results of assignments and tests. This informal CCDL semantics is formalized by intuitionistic Kripke frames modeling this partial information, and each such frame is interpreted as an idealized concurrent machine . In CCDL, proofs and deductions are ω-height, ω-branching, well-founded labeled subtrees of ωω. These are a generalization of the signed tableaux of Nerode [A. Nerode, Some lectures in modal logic, Technical Report, M.S.I. Cornell University, 1989, CIME Logic and Computer Science Montecatini Volume, Springer-Verlag Lecture Notes, 1990, A. Nerode, Some lectures in intuitionistic logic, Technical Report, M.S.I. Cornell University, 1988, Marktoberdorf Logic and Computation NATO Summer School Volume, NATO Science Series, 1990 ] stemming from the prefix tableaux of Fitting [M.C. Fitting, Proof Methods for Modal and Intuitionistic Logic, Reidel, 1983]. We demonstrate the correctness of our tableau proofs, define consistency properties, prove that consistency properties yield models, construct systematic tableaux, prove that systematic tableaux yield a consistency property, and conclude that CCDL is complete. This infinitary semantics and proof procedure will be the primary guide for defining, in a sequel, the correct finitary CCDL based on induction principles. FCCDL is suitable for implementation in constructive logic software systems such as Constable’s NUPRL or Huet-Coquand’s CONSTRUCTIONS. Our goal is to develop a constructive logic programming tool for specification and modular verification of programs in any imperative concurrent language, and for the extraction of concurrent programs from constructive proofs. Subsequent papers will introduce analogous logics for declarative and functional concurrent languages. (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)

In this work, we shall study structural abduction and how ways of searching for solutions to the corresponding abductive problems could be modeled. Specifically, we shall define modal semantic tableaux for normal modal systems and study its applications to structural abduction. This method even makes structural abduction clearer and, as it shall be seen, when a radical change of logic is epistemologically required, the corresponding tableau will have pertinent information to suggest it.

This paper, we propose a modal logic satisfying minimal requirements for reasoning about diagrams via collection of sets and relations between them, following Harel's proposal. We first give an axiomatics of such a theory and then provide its Kripke semantics. Then we extend previous works of ours in order to obtain a decision procedure based on tableaux for this logic. Beside soundness and completeness of our tableaux, we manage to define a strategy of rule application ensuring termination by (...) extending the usual loop test of modal logic S4 to whole sub-structures of the model being computed. (shrink)

Free-variable semantic tableaux are a well-established technique for first-order theorem proving where free variables act as a meta-linguistic device for tracking the eigenvariables used during proof search. We present the theoretical foundations to extend this technique to propositional modal logics, including non-trivial rigorous proofs of soundness and completeness, and also present various techniques that improve the efficiency of the basic naive method for such tableaux.

The paper is concerned with the psychological relevance of a logical model for deductive reasoning. We propose a new way to analyze logical reasoning in a deductive version of the Mastermind game implemented within a popular Dutch online educational learning system (Math Garden). Our main goal is to derive predictions about the difficulty of Deductive Mastermind tasks. By means of a logical analysis we derive the number of steps needed for solving these tasks (a proxy for working memory load). Our (...) model is based on the analytic tableaux method, known from proof theory. We associate the difficulty of Deductive Mastermind game-items with the size of the corresponding logical trees obtained by the tableaux method. We derive empirical hypotheses from this model. A large group of students (over 37 thousand children, 5–12 years of age) played the Deductive Mastermind game, which gave empirical difficulty ratings of all 321 game-items. The results show that our logical approach predicts these item ratings well, which supports the psychological relevance of our model. (shrink)

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.

This is an examination of similarities and differences between Atocha Aliseda’s semantic tableaux analysis of abduction and Dov Gabbay’s and the present author’s ignorance-preservation model of it. Also discussed is the suitability of these models for the analysis of the logical structure of legal reasoning.

From picture to photography and back. Tableau vivants, in their gestural synthetic dimension, represent for Diderot the apex of expression that the image can make explicit. Nothing closer to Wall’s poetics. His works show outstanding attention to detail: from scenic design to protagonists’ costumes, from light to actors’ action. And the result is exactly what Diderot saw in the eyes of people observing Chardin’s art: imagination at work.

We introduce reactive Kripke models for intuitionistic logic and show that the reactive semantics is stronger than the ordinary semantics. We develop Beth tableaux for the reactive semantics.

The formalization of abductive reasoning has received increasing attention from logicians. However, few work is found beyond abduction in propositional logic, given that in a first order formalism, the undecidability problem naturally appears, and therefore an abductive problem cannot even be appropriately formulated. Still, many applications in artificial intelligence allow finite domains to work with, and this gives an opportunity to apply abduction in first order logic with restricted domains. In this paper, we present an approach to abductive reasoning in (...) C-structures, first order structures with a finite domain in which each of its elements has a corresponding constant representing its interpretation. By using semantic tableaux with bounded depth, that is, C-tableaux (a modification of N-tableaux, introduced by the authors in previous papers) and δ-resolution calculus, we build an effective procedure for the searching of minimal abductive solutions within the proposed semantics. (shrink)

Interval temporal logics provide both an insight into a nature of time and a framework for temporal reasoning in various areas of computer science. In this paper we present sound and complete relational proof systems in the style of dual tableaux for relational logics associated with modal logics of temporal intervals and we prove that the systems enable us to verify validity and entailment of these temporal logics. We show how to incorporate in the systems various relations between intervals (...) and/or various time orderings. (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)

Throughout the last decade, there has been an increased interest in various forms of dynamic epistemic logics to model the flow of information and the effect this flow has on knowledge in multi-agent systems. This enterprise, however, has mostly been applicationally and semantically driven. This results in a limited amount of proof theory for dynamic epistemic logics. In this paper, we try to compensate for a part of this by presenting terminating tableau systems for full dynamic epistemic logic with action (...) models and for a hybrid public announcement logic. The tableau systems are extensions of already existing tableau systems, in addition to which we have used the reduction axioms of dynamic epistemic logic to define rules for the dynamic part of the logics. Termination is shown using methods introduced by Braüner, Bolander, and Blackburn. (shrink)

The inference systems proposed for solving SAT are unsound for solving MaxSAT and MinSAT, because they preserve satisfiability but not the minimum and maximum number of clauses that can be falsified, respectively. To address this problem, we first define a clause tableau calculus for MaxSAT and prove its soundness and completeness. We then define a clause tableau calculus for MinSAT and also prove its soundness and completeness. Finally, we define a complete clause tableau calculus for solving both MaxSAT and MinSAT, (...) in that the minimum number of generated empty clauses provides an optimal MaxSAT solution and the maximum number provides an optimal MinSAT solution. (shrink)

As a remedy for the bad computational behaviour of first-order temporal logic (FOTL), it has recently been proposed to restrict the application of temporal operators to formulas with at most one free variable thereby obtaining so-called monodic fragments of FOTL. In this paper, we are concerned with constructing tableau algorithms for monodic fragments based on decidable fragments of first-order logic like the two-variable fragment or the guarded fragment. We present a general framework that shows how existing decision procedures for first-order (...) fragments can be used for constructing a tableau algorithm for the corresponding monodic fragment of FOTL. Some example instantiations of the framework are presented. (shrink)

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.

In 1944 Hans Reichenbach developed a three-valued propositional logic (RQML) in order to account for certain causal anomalies in quantum mechanics. In this logic, the truth-value _indeterminate_ is assigned to those statements describing physical phenomena that cannot be understood in causal terms. However, Reichenbach did not develop a deductive calculus for this logic. The aim of this paper is to develop such a calculus by means of First Degree Entailment logic (FDE) and to prove it sound and complete with respect (...) to RQML semantics. In Section 1 we explain the main physical and philosophical motivations of RQML. Next, in Sections 2 and 3, respectively, we present RQML and FDE syntax and semantics and explain the relation between both logics. Section 4 introduces \(\varvec{\mathcal {Q}}\) calculus, an FDE-based tableaux calculus for RQML. In Section 5 we prove that \(\varvec{\mathcal {Q}}\) calculus is sound and complete with respect to RQML three-valued semantics. Finally, in Section 6 we consider some of the main advantages of \(\varvec{\mathcal {Q}}\) calculus and we apply it to Reichenbach’s analysis of causal anomalies. (shrink)

In this paper we present a tableau system for deontic logics with the operator of explicit permission. By means of this system the decidability of the considered logics can be proved. We will sketch how these logics are semantically defined by means of relating semantics and how they provide a simple solution to the free choice permission problem. In short, these logics employ relating implication and a certain propositional constant. These two are in turn used to define deontic operators similarly (...) as in Andersonian-Kangerian reduction, which uses different intensional implications and constants. (shrink)

We present two proof systems for first-order logic with identity and without function symbols. The first one is an extension of the Rasiowa-Sikorski system with the rules for identity. This system is a validity checker. The rules of this system preserve and reflect validity of disjunctions of their premises and conclusions. The other is a Tableau system, which is an unsatisfiability checker. Its rules preserve and reflect unsatisfiability of conjunctions of their premises and conclusions. We show that the two systems (...) are dual to each other. The duality is expressed in a formal way which enables us to define a transformation of proofs in one of the systems into the proofs of the other. (shrink)

We present a new proof of soundness/completeness of tableaux with respect to dialogical games in Classical First-Order Logic. As far as we know it is the first thorough result for dialogical games where finiteness of plays is guaranteed by means of what we call repetition ranks.

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)

We present tableau proof systems for the annotated version of propositional justification logics, that is, justification logics which are formulated using annotated application operators. We show that the tableau systems are sound and complete with respect to Mkrtychev models, and some tableau systems are analytic and provide a decision procedure for the annotated justification logics. We further show Craig’s interpolation property and Beth’s definability theorem for some annotated justification logics.