Classical Logic—Basic Tableaus

  • Melvin Fitting
Part of the Trends in Logic book series (TREN, volume 12)


Several varieties of proof procedures have been developed for firstorder classical logic. Among them the semantic tableau procedure has a considerable attraction, [Smu68, Fit96] . It is intuitive, close to the intended semantics, and is automatable. For higher-order classical logic, semantic tableaus are not as often seen—most treatments in the literature are axiomatic. Among the notable exceptions are [ToI75, Smi93, Koh95, GilOl] . In fact, semantic tableaus retain much of their first-order ability to charm, and they are what I present here. Automatability becomes more problematic, however, for reasons that will become clear as we proceed. Consequently the presentation should be thought of as meant for human use, and intelligence in the construction of proofs is expected.


Free Variable Classical Logic Existential Quantifier Universal Rule Kripke Semantic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media Dordrecht 2002

Authors and Affiliations

  • Melvin Fitting
    • 1
  1. 1.Lehman College and the Graduate CenterCity University of New YorkUSA

Personalised recommendations