Automated natural deduction in thinker

Studia Logica 60 (1):3-43 (1998)
  Copy   BIBTEX


Although resolution-based inference is perhaps the industry standard in automated theorem proving, there have always been systems that employed a different format. For example, the Logic Theorist of 1957 produced proofs by using an axiomatic system, and the proofs it generated would be considered legitimate axiomatic proofs; Wang’s systems of the late 1950’s employed a Gentzen-sequent proof strategy; Beth’s systems written about the same time employed his semantic tableaux method; and Prawitz’s systems of again about the same time are often said to employ a natural deduction format. [See Newell, et al (1957), Beth (1958), Wang (1960), and Prawitz et al (1960)]. Like sequent proof systems and tableaux proof systems, natural deduction systems retain..



    Upload a copy of this work     Papers currently archived: 83,878

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

The Geometry of Non-Distributive Logics.Greg Restall & Francesco Paoli - 2005 - Journal of Symbolic Logic 70 (4):1108 - 1126.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Two natural deduction systems for hybrid logic: A comparison. [REVIEW]Torben Braüner - 2004 - Journal of Logic, Language and Information 13 (1):1-23.
Sequent calculus in natural deduction style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.
A Brief History of Natural Deduction.Francis Jeffry Pelletier - 1999 - History and Philosophy of Logic 20 (1):1-31.


Added to PP

90 (#153,980)

6 months
6 (#145,517)

Historical graph of downloads
How can I increase my downloads?

References found in this work

First-order logic.Raymond Merrill Smullyan - 1968 - New York [etc.]: Springer Verlag.
First-order Logic.William Craig - 1975 - Journal of Symbolic Logic 40 (2):237-238.
Logic: Techniques of Formal Reasoning.Donald Kalish, Richard Montague & Gary Mar - 1964 - New York, NY, USA: Oxford University Press USA. Edited by Richard Montague.
Logic.Donald Kalish - 1964 - New York,: Harcourt, Brace & World. Edited by Richard Montague.
How to reason defeasibly.John L. Pollock - 1992 - Artificial Intelligence 57 (1):1-42.

View all 17 references / Add more references