TPS: A hybrid automatic-interactive system for developing proofs

&
Journal of Applied Logic 4 (4):367-395 (2006)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.1016/j.jal.2005.10.002

Other Versions

No versions found

Links

PhilArchive

External links

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

Through your library

My notes

Similar books and articles

Reasoning in simple type theory – Festschrift in honor of Peter B. Andrews on his 70th birthday, edited by Christoph Benzmüller, Chad E. Brown, Jörg Siekmann, and Richard Statman, Studies in Logic, vol. 17. College Publications, London, 2008, 454 pp. [REVIEW]Florian Rabe - 2010 - Bulletin of Symbolic Logic 16 (3):409-411.
Integrating TPS and OMEGA.Christoph Benzmüller, Matt Bishop & Volker Sorge - 1999 - Journal of Universal Computer Science 5 (3):188-207.
Peter B. Andrews. An introduction to mathematical logic and type theory: to truth through proof. Computer science and applied mathematics. Academic Press, Orlando etc. 1986, xv + 304 pp.M. Yasuhara - 1988 - Journal of Symbolic Logic 53 (1):312-314.
Interactive proof-search for equational reasoning.Favio E. Miranda-Perea, Lourdes del Carmen González Huesca & P. Selene Linares-Arévalo - forthcoming - Logic Journal of the IGPL.
Andrews Peter B.. An introduction to mathematical logic and type theory: to truth through proof. Applied logic series, vol. 27. Kluwer Academic Publishers, Dordrecht, Boston, and London, 2002, xviii+ 390 pp. [REVIEW]Mitsuru Yasuhara - 2003 - Bulletin of Symbolic Logic 9 (3):408-408.
Challenging epistemology: Interactive proofs and zero knowledge.Justin Bledin - 2008 - Journal of Applied Logic 6 (4):490-501.
Automatic knowledge learning and case adaptation with a hybrid committee approach.Claudio A. Policastro, Andre C. P. L. F. Carvalho & Alexandre C. B. Delbem - 2006 - Journal of Applied Logic 4 (1):26-38.
Peter B. Andrews. Resolution with merging. Journal of the Association for Computing Machinery, vol. 15 , pp. 367–381.David Luckham - 1970 - Journal of Symbolic Logic 35 (1):159-160.
Reasoning in simple type theory — Festschrift in honor of Peter B. Andrews on his 70th birthday, Studies in Logic, vol. 17. [REVIEW]Christoph Benzmüller, Chad E. Brown, Jörg Siekmann & Richard Statman - 2010 - Bulletin of Symbolic Logic 16 (3):409-411.
Automatic proof generation in an axiomatic system for $\mathsf{CPL}$ by means of the method of Socratic proofs.Aleksandra Grzelak & Dorota Leszczyńska-Jasion - 2018 - Logic Journal of the IGPL 26 (1):109-148.

Analytics

Added to PP
2016-06-30

Downloads
63 (#953,873)

6 months
10 (#1,162,156)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Computational Philosophy.Patrick Grim & Daniel Singer - 2024 - Stanford Encyclopedia of Philosophy.
Quantum Trans-statistics from an Ontology of Properties.Sebastian Fortin & Matías Pasqualini - 2023 - Revista Colombiana de Filosofía de la Ciencia 23 (47):255-291.

Add more citations

References found in this work

Resolution in type theory.Peter B. Andrews - 1971 - Journal of Symbolic Logic 36 (3):414-432.
A compact representation of proofs.Dale A. Miller - 1987 - Studia Logica 46 (4):347 - 370.
A man-machine theorem-proving system.W. W. Bledsoe & Peter Bruell - 1974 - Artificial Intelligence 5 (1):51-72.

Add more references