The liberalized \(\delta\)-rule in free variable semantic tableaux
type: Item
instance of: scholarly article
title: The liberalized \(\delta\)-rule in free variable semantic tableaux
zbMATH Open document ID: 0826.03005
DOI: 10.1007/BF00881956
author: Reiner Hähnle
author: Peter H. Schmitt
published in: Journal of Automated Reasoning
publication date: 1995-02-22T00:00:00Z
review text: The liberalized \(\delta\)-rule in free variable semantic tableaux is studied. This rule was presented by Smullyan. The authors consider a modification of this rule, called the \(\delta+\)-rule, which uses fewer free variables. The relationship between the \(\delta+\)-rule and variations of the \(\delta\)-rule is studied. The problem lies in proving the correctness of the \(\delta+\)-rule. The main result (soundness) is the following: If a sentence \(X\) has a closed tableau \(T\) constructed with \(\delta+\), then \(X\) is not satisfiable.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 724141
zbMATH Keywords: soundness
zbMATH Keywords: semantic tableaux
zbMATH Keywords: \(\delta+\)-rule
zbMATH Keywords: correctness
reviewed by: Andrzej Biela
MaRDI profile type: Publication
cites work: Q4275685
cites work: Situations, language and logic
cites work: First-order modal tableaux
cites work: Q3996619
cites work: Negation in logic programming
cites work: Q5560258
full work available at URL: https://doi.org/10.1007/bf00881956
OpenAlex ID: W1993434661
description: scientific article; zbMATH DE number 724141