Advertisement

Springer Nature is making Coronavirus research free. View research | View latest news | Sign up for updates

The liberalized δ-rule in free variable semantic tableaux

  • 40 Accesses

  • 37 Citations

Abstract

In this paper we have a closer look at one of the rules of the tableau calculus presented by Fitting [4], 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 [9]. 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.

References

  1. 1.

    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).

  2. 2.

    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).

  3. 3.

    Fitting, Melvin C., ‘First-order modal tableaux’,J. Automated Reasoning 4, 191–213 (1988).

  4. 4.

    Fitting, Melvin C.,First-Order Logic and Automated Theorem Proving, Springer, New York (1990).

  5. 5.

    Hähnle, Reiner, ‘Uniform notation of tableaux rules for multiple-valued logics’, inProc. International Symposium on Multiple-Valued Logic, Victoria (1991), pp. 238–245.

  6. 6.

    Kunen, Kenneth, ‘Negation in logic programming’,J. Logic Programming 4, 289–308 (1987).

  7. 7.

    MacNish, Craig and Fallside, Frank, ‘Asserted 3-valued logic for default reasoning’, CUED/F-INFENG/TR.40, Department of Engineering, University of Cambridge (1990).

  8. 8.

    Reeves, Steve V., ‘Semantic tableaux as a framework for automated theorem-proving’, Department of Computer Science and Statistics, Queen Mary College, Univ. London (1987).

  9. 9.

    Smullyan, Raymond,First-Order Logic. 2nd edn, Springer, New York (1968).

Download references

Author information

Rights and permissions

Reprints and Permissions

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

Download citation

Key words

  • Mechanical theorem proving
  • tableau calculus