Gts and interrogative tableaux

A variant of the standard deductive tableau system is introduced, and interrogative rules are added, resulting in a so-called interrogative tableau system. A game-theoretical account of entailment is sketched, and the deductive tableau system is interpreted in these terms. Finally, it is shown how to extend this account of entailment into an account of interrogative entailment, thereby providing a semantics for the interrogative tableau system.     

SLAP: Specification logic of actions with probability

A logic for specifying probabilistic transition systems is presented. Our perspective is that of agents performing actions. A procedure for deciding whether sentences in this logic are valid is provided. One of the main contributions of the paper is the formulation of the decision procedure: a tableau system which appeals to solving systems of linear equations. The tableau rules eliminate propositional connectives, then, for all open branches of the tableau tree, systems of linear equations are generated and checked for feasibility. Proofs of soundness, completeness and termination of the decision procedure are provided.     

概称句词项逻辑的树图判定算法

概称句的形式刻画研究始于人工智能。从条件蕴涵引入开始,到建立概称句词项逻辑的形式系统GAG和Gaa,关于概称句这一系列的研究主要是围绕概称句自身性质的探讨,以试图对于概称句推理给出更合理的形式刻画,而没有同时兼顾计算机应用方面的考虑。回归问题的初始,关于概称句的概念理论是否还可以用于计算机科学领域,是这一研究路线所面临的问题。首先要解决的问题是,根据GAG和Gaa模型,公式的可满足性是否有能行的判定方法。对此本文给出了基于GAG语义的树图判定算法,包括相应的可靠性,完备性等证明。     

Tableau reductions: Towards an optimal decision procedure for the modal necessity

We present a new prefixed tableau system $\mathsf{TK}$ for verification of validity in modal logic $\mathsf{K}$. The system $\mathsf{TK}$ is deterministic, it uniquely generates exactly one proof tree for each clausal representation of formulas, and, moreover, it uses some syntactic reductions of prefixes. $\mathsf{TK}$ is defined in the original methodology of tableau systems, without any external technique such as backtracking, backjumping, etc. Since all the necessary bookkeeping is built into the rules, the system is not only a basis for a validity algorithm, but is itself a decision procedure. We present also a deterministic tableau decision procedure which is an extension of $\mathsf{TK}$ and can be used for the global assumptions problem.     

An Axiomatic System and a Tableau Calculus for STIT Imagination Logic

We formulate a Hilbert-style axiomatic system and a tableau calculus for the STIT-based logic of imagination recently proposed in Wansing (2015). 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.     

An analytic tableau calculus for a temporalised belief logic

A tableau is a refutation-based decision procedure for a related logic, and is among the most popular proof procedures for modal logics. In this paper, we present a labelled tableau calculus for a temporalised belief logic called TML⁺, which is obtained by adding a linear-time temporal logic onto a belief logic by the temporalisation method of Finger and Gabbay. We first establish the soundness and the completeness of the labelled tableau calculus based on the soundness and completeness results of its constituent logics. We then sketch a resolution-type proof procedure that complements the tableau calculus and also propose a model checking algorithm for TML⁺ based on the recent results for model checking procedures for temporalised logics. TML⁺ is suitable for formalising trust and agent beliefs and reasoning about their evolution for agent-based systems. Based on the logic TML⁺, the proposed labelled tableau calculus could be used for analysis, design and verification of agent-based systems operating in dynamic environments.     

Free Semantics

Free Semantics is based on normalized natural deduction for the weak relevant logic DW and its near neighbours. This is motivated by the fact that in the determination of validity in truth-functional semantics, natural deduction is normally used. Due to normalization, the logic is decidable and hence the semantics can also be used to construct counter-models for invalid formulae. The logic DW is motivated as an entailment logic just weaker than the logic MC of meaning containment. DW is the logic focussed upon, but the results extend to MC. The semantics is called ‘free semantics’ since it is disjunctively and existentially free in that no disjunctive or existential witnesses are produced, unlike in truth-functional semantics. Such ‘witnesses’ are only assumed in generality and are not necessarily actual. The paper sets up the free semantics in a truth-functional style and gives a natural deduction interpetation of the meta-logical connectives. We then set out a familiar tableau-style system, but based on natural deduction proof rather than truth-functional semantics. A proof of soundness and completeness is given for a reductio system, which is a transform of the tableau system. The reductio system has positive and negative rules in place of the elimination and introduction rules of Brady’s normalized natural deduction system for DW. The elimination-introduction turning points become closures of threads of proof, which are at the points of contradiction for the reductio system.     

A general tableau method for propositional interval temporal logics: Theory and implementation

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 (BCDT⁺ 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.     

Analytic Tableaux for all of <Emphasis Type="Italic">SIXTEEN</Emphasis><Subscript>3</Subscript>

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.     

Theory matrices (for modal logics) using alphabetical monotonicity

In this paper I give conditions under which a matrix characterisation of validity is correct for first order logics where quantifications are restricted by statements from a theory. Unfortunately the usual definition of path closure in a matrix is unsuitable and a less pleasant definition must be used. I derive the matrix theorem from syntactic analysis of a suitable tableau system, but by choosing a tableau system for restricted quantification I generalise Wallen's earlier work on modal logics. The tableau system is only correct if a new condition I call alphabetical monotonicity holds. I sketch how the result can be applied to a wide range of logics such as first order variants of many standard modal logics, including non-serial modal logics.     

Simultaneous Rigid Sorted Unification for Tableaux

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.     

Controlled attending as a function of melodic and temporal context

Melodic and rhythmic context were systematically varied in a pattern recognition task involving pairs (standard-comparison) of nine-tone auditory sequences. The experiment was designed to test the hypothesis that rhythmic context can direct attention toward or away from tones which instantiate higher order melodic rules. Three levels of melodic structure (one, two, no higher order rules) were crossed with four levels of rhythm [isochronous, dactyl (A U U), anapest (U U A), irregular]. Rhythms were designed to shift accent locations on three centrally embedded tones. Listeners were more accurate in detecting violations of higher order melodic rules when the rhythmic context induced accents on tones which instantiated these rules. Effects are discussed in terms of attentional rhythmicity.     

A robot’s sense-making of fallacies and rhetorical tropes. Creating ontologies of what humans try to say

In the design of user-friendly robots, human communication should be understood by the system beyond mere logics and literal meaning. Robot communication-design has long ignored the importance of communication and politeness rules that are ‘forgiving’ and ‘suspending disbelief’ and cannot handle the basically metaphorical way humans design their utterances. Through analysis of the psychological causes of illogical and non-literal statements, signal detection, fundamental attribution errors, and anthropomorphism, we developed a fail-safe protocol for fallacies and tropes that makes use of Frege’s distinction between reference and sense, Beth’s tableau analytics, Grice’s maxim of quality, and epistemic considerations to have the robot politely make sense of a user’s sometimes unintelligible demands.     

Analytic Tableau Systems and Interpolation for the Modal Logics KB, KDB, K5, KD5

We give complete sequent-like tableau systems for the modal logics KB, KDB, K5, and KD5. Analytic cut rules are used to obtain the completeness. Our systems have the analytic superformula property and can thus give a decision procedure. Using the systems, we prove the Craig interpolation lemma for the mentioned logics.     

Connection Tableau Calculi with Disjunctive Constraints

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 the efficient handling of constraints during the search process. The new techniques are integrated into the automated connection tableau prover Setheo.     

Tableaux for Łukasiewicz Infinite-valued Logic

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     

Shortcuts and Dynamic Marking in the Tableau Method for Adaptive Logics

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.     

FOIL Axiomatized

In an earlier paper, [5], I gave semantics and tableau rules for a simple firstorder intensional logic called FOIL, in which both objects and intensions are explicitly present and can be quantified over. Intensions, being non-rigid, are represented in FOIL as (partial) functions from states to objects. Scoping machinery, predicate abstraction, is present to disambiguate sentences like that asserting the necessary identity of the morning and the evening star, which is true in one sense and not true in another.In this paper I address the problem of axiomatizing FOIL. I begin with an interesting sublogic with predicate abstraction and equality but no quantifiers. In [2] this sublogic was shown to be undecidable if the underlying modal logic was at least K4, though it is decidable in other cases. The axiomatization given is shown to be complete for standard logics without a symmetry condition. The general situation is not known. After this an axiomatization for the full FOIL is given, which is straightforward after one makes a change in the point of view.This paper is a version of the invited talk given by the author at the conference Trends in Logic III, dedicated to the memory of A. MOSTOWSKI, H. RASIOWA and C. RAUSZER, and held in Warsaw and Ruciane-Nida from 23rd to 25th September 2005.