A Tableau System for Instantial Neighborhood Logic

2017 ◽  
pp. 337-353 ◽  
Author(s):  
Junhua Yu
Keyword(s):  
Tableau System

scholarly journals Deduction in Non-Fregean Propositional Logic SCI

Axioms ◽  
2019 ◽  
Vol 8 (4) ◽  
pp. 115 ◽  
Author(s):  
Joanna Golińska-Pilarek ◽  
Magdalena Welle
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Classical Propositional Logic ◽  
Tableau System ◽  
Soundness And Completeness

We study deduction systems for the weakest, extensional and two-valued non-Fregean propositional logic SCI . The language of SCI is obtained by expanding the language of classical propositional logic with a new binary connective ≡ that expresses the identity of two statements; that is, it connects two statements and forms a new one, which is true whenever the semantic correlates of the arguments are the same. On the formal side, SCI is an extension of classical propositional logic with axioms characterizing the identity connective, postulating that identity must be an equivalence and obey an extensionality principle. First, we present and discuss two types of systems for SCI known from the literature, namely sequent calculus and a dual tableau-like system. Then, we present a new dual tableau system for SCI and prove its soundness and completeness. Finally, we discuss and compare the systems presented in the paper.

A Set-theoretic Approach to Reasoning Services for the Description Logic 𝒟 ℒ D 4,×

2020 ◽  
Vol 176 (3-4) ◽  
pp. 349-384
Author(s):  
Domenico Cantone ◽  
Marianna Nicolosi-Asmundo ◽  
Daniele Francesco Santamaria
Keyword(s):  
Description Logic ◽  
Description Logics ◽  
Theoretic Approach ◽  
The Novel ◽  
Data Types ◽  
Left Hand ◽  
Rule Languages ◽  
Tableau System ◽  
High Scalability ◽  
Better Than

In this paper we consider the most common TBox and ABox reasoning services for the description logic 𝒟ℒ〈4LQSR,x〉(D) ( 𝒟 ℒ D 4,× , for short) and prove their decidability via a reduction to the satisfiability problem for the set-theoretic fragment 4LQSR. 𝒟 ℒ D 4,× is a very expressive description logic. It combines the high scalability and efficiency of rule languages such as the SemanticWeb Rule Language (SWRL) with the expressivity of description logics. In fact, among other features, it supports Boolean operations on concepts and roles, role constructs such as the product of concepts and role chains on the left-hand side of inclusion axioms, role properties such as transitivity, symmetry, reflexivity, and irreflexivity, and data types. We further provide a KE-tableau-based procedure that allows one to reason on the main TBox and ABox reasoning tasks for the description logic 𝒟 ℒ D 4,× . Our algorithm is based on a variant of the KE-tableau system for sets of universally quantified clauses, where the KE-elimination rule is generalized in such a way as to incorporate the γ-rule. The novel system, called KEγ-tableau, turns out to be an improvement of the system introduced in [1] and of standard first-order KE-tableaux [2]. Suitable benchmark test sets executed on C++ implementations of the three mentioned systems show that in several cases the performances of the KEγ-tableau-based reasoner are up to about 400% better than the ones of the other two systems.

A Seligman-Style Tableau System

2013 ◽  
pp. 147-163 ◽  
Author(s):  
Patrick Blackburn ◽  
Thomas Bolander ◽  
Torben Braüner ◽  
Klaus Frovin Jørgensen
Keyword(s):  
Tableau System

scholarly journals Completeness and termination for a Seligman-style tableau system

2015 ◽  
Vol 27 (1) ◽  
pp. 81-107
Author(s):  
Patrick Blackburn ◽  
Thomas Bolander ◽  
Torben Braüner ◽  
Klaus Frovin Jørgensen
Keyword(s):  
Tableau System

scholarly journals Tableau Calculus for Dummett Logic Based on Present and Next State of Knowledge

10.29007/dhz5 ◽  
2018 ◽  
Author(s):  
Guido Fiorino
Keyword(s):  
Intuitionistic Logic ◽  
Search Space ◽  
Kripke Semantics ◽  
Proof Systems ◽  
Dummett Logic ◽  
Intermediate Logics ◽  
Tableau System

In this paper we use the Kripke semantics characterization of Dummett logic to introduce a new way of handling non-forced formulas in tableau proof systems. We pursue the aim of reducing the search space by strictly increasing the number of forced propositional variables after the application of non-invertible rules. The focus of the paper is on a new tableau system for Dummett logic, for which we have an implementation. The ideas presented can be extended to intuitionistic logic and intermediate logics as well.

scholarly journals Analytic tableaux and interpolation

2007 ◽  
pp. 93-97
Author(s):  
Miodrag Kapetanovic
Keyword(s):  
Predicate Logic ◽  
Interpolation Theorem ◽  
Analytic Tableaux ◽  
Tableau System

A tableau system for the predicate logic with countable conjunctions and disjunctions is presented and the completeness of the set of rules proved. These tableaux are used to prove a slightly more general form of the Malitz interpolation theorem.

The Tableau System

1992 ◽  
pp. 30-50
Author(s):  
Julian Charles Bradfield
Keyword(s):  
Tableau System
Sign in / Sign up

Export Citation Format

Share Document