In this paper we have a closer look at one of the rules of the tableau calculus presented by Fitting , called the δ-rule. We prove that a modification of this rule, called the δ+-rule, which uses fewer free variables, is also sound and complete. We examine the relationship between the δ+-rule and variations of the δ-rule presented by Smullyan . This leads to a second proof of the soundness of the δ+-rule. An example shows the relevance of this modification for building tableau-based theorem provers.
This is a preview of subscription content, log in to check access.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
Doherty, Patrick and Lukaszewicz, Witold, ‘NML3 — a non-monotonic logic with explicit defaults’, Research Report, RKLLAB LiTH-IDA-R-91-13, Dept. of Computer and Information Science, Linköping University (1991).
Fenstad, Jens Erik, Halvorsen, Per-Kristian, Langholm, Tore and Benthem, Johan van, ‘Equations, schemata and situations: A framework for linguistic semantics’, Technical Report CSLI-85-29, Center for the Studies of Language and Information Stanford (1985).
Fitting, Melvin C., ‘First-order modal tableaux’,J. Automated Reasoning 4, 191–213 (1988).
Fitting, Melvin C.,First-Order Logic and Automated Theorem Proving, Springer, New York (1990).
Hähnle, Reiner, ‘Uniform notation of tableaux rules for multiple-valued logics’, inProc. International Symposium on Multiple-Valued Logic, Victoria (1991), pp. 238–245.
Kunen, Kenneth, ‘Negation in logic programming’,J. Logic Programming 4, 289–308 (1987).
MacNish, Craig and Fallside, Frank, ‘Asserted 3-valued logic for default reasoning’, CUED/F-INFENG/TR.40, Department of Engineering, University of Cambridge (1990).
Reeves, Steve V., ‘Semantic tableaux as a framework for automated theorem-proving’, Department of Computer Science and Statistics, Queen Mary College, Univ. London (1987).
Smullyan, Raymond,First-Order Logic. 2nd edn, Springer, New York (1968).
About this article
Cite this article
Hähnle, R., Schmitt, P.H. The liberalized δ-rule in free variable semantic tableaux. J Autom Reasoning 13, 211–221 (1994). https://doi.org/10.1007/BF00881956
- Mechanical theorem proving
- tableau calculus