Efficiently checking propositional refutations in HOL theorem provers

&
Journal of Applied Logic 7 (1):26-40 (2009)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.1016/j.jal.2007.07.003

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,202

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

Regressive Merging in Model Elimination Tableau-Based Theorem Provers.Kevin Wallace & Graham Wrightson - 1995 - Logic Journal of the IGPL 3 (6):921-937.
An empirical analysis of modal theorem provers.Ullrich Hustadt & Renate A. Schmidt - 1999 - Journal of Applied Non-Classical Logics 9 (4):479-522.
Automated theorem proving for łukasiewicz logics.Gordon Beavers - 1993 - Studia Logica 52 (2):183 - 195.
Natural deduction.John Pollock - manuscript
The Triumph of Types: Principia Mathematica's Impact on Computer Science.Robert L. Constable - unknown
Best-Path Theorem Proving: Compiling Derivations.Martin Frické Frické - 2012 - In James Maclaurin (ed.), Rationis Defensor.
A proof of axiomatizability of łukasiewicz’s three-valued implicational propositional calculus.T. Prucnal - 1967 - Studia Logica 20 (1):144-144.
Extended full computation-tree logics for paraconsistent model checking.Norihiro Kamide - 2007 - Logic and Logical Philosophy 15 (3):251-276.
How to avoid the formal verification of a theorem prover.A. Avellone, M. Benini & U. Moscato - 2001 - Logic Journal of the IGPL 9 (1):1-25.
Contraction-elimination for implicational logics.Ryo Kashima - 1997 - Annals of Pure and Applied Logic 84 (1):17-39.
Theorem proving for untyped constructive λ-calculus: implementation and application.A. Ramsay - 2001 - Logic Journal of the IGPL 9 (1):83-100.
New sequent calculi for Visser's Formal Propositional Logic.Katsumasa Ishii - 2003 - Mathematical Logic Quarterly 49 (5):525.
A finite model theorem for the propositional μ-calculus.Dexter Kozen - 1988 - Studia Logica 47 (3):233 - 241.
Theorem provers with counter-models and xpe.Motohiko Mouri - 2001 - Bulletin of the Section of Logic 30 (2):79-86.
Resolution for Intuitionistic Logic.Melvin Fitting - unknown

Analytics

Added to PP
2016-06-30

Downloads
8 (#1,249,165)

6 months
5 (#544,079)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references