A Compressing Translation from Propositional Resolution to Natural Deduction
Author: 
Hasan AmjadAuthors Info & Claims
Pages 88 - 102
Abstract
We describe a translation from SAT solver generated propositional resolution refutation proofs to classical natural deduction proofs. The resulting proof can usually be checked quicker than one that simply simulates the original resolution proof. We use this result in interactive theorem provers, to speed up reconstruction of SAT solver generated proofs. The translation is efficient, running in time linear in the length of the original proof, and effective, easily scaling up to large proofs with millions of inferences.
References
[1]
Alekhnovich, M., Razborov, A.A.: Resolution is not automatizable unless W{P} is tractable. In: FOCS, pp. 210-219. IEEE Computer Society Press, Los Alamitos (2001)
[2]
Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 167-181. Springer, Heidelberg (2006)
[3]
Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A theorem-proving environment for higher order logic. Cambridge University Press, Cambridge (1993)
[4]
Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI International (1995)
[5]
Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265-269. Springer, Heidelberg (1996)
[6]
Harrison, J.: Stålmarck's algorithm as a HOL derived rule. In: von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 221-234. Springer, Heidelberg (1996)
[7]
Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq proof assistant: A tutorial: Version 7.2. Technical Report RT-0256, INRIA (February 2002)
[8]
Mitchell, D.G.: A SAT solver primer. In: EATCS Bulletin (The Logic in Computer Science Column), vol. 85, pp. 112-133 (February 2005)
[9]
Morrison, D.R.: PATRICIA-Practical Algorithm To Retrieve Information Code. In Alphanumeric. J. ACM 15(4), 514-534 (1968)
[10]
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, pp. 530-535. ACM Press, New York (2001)
[11]
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748-752. Springer, Heidelberg (1992)
[12]
Paulson, L.C.: A Generic Theorem Prover. In: Paulson, L.C. (ed.) Isabelle. LNCS, vol. 828, Springer, Heidelberg (1994)
[13]
Shankar, N.: Using decision procedures with a higher-order logic. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 5-26. Springer, Heidelberg (2001)
[14]
Sinz, C.: Compressing propositional proofs by common subproof extraction. In: Pichler, F. (ed.) Euro Conference on Computer Aided Systems Theory (2007)
[15]
Ukkonen, E.: Online construction of suffix trees. Algorithmica 14(3), 249-260 (1995)
[16]
Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. JAL (special issue on Empirically Successful Computerized Reasoning) (to appear, 2007)
- A Compressing Translation from Propositional Resolution to Natural Deduction
Recommendations
Peirce's rule in natural deduction
In stark contrast to Natural Deduction for Intuitionistic Logic, Natural Deduction for Classical Logic suffers from some well-known limitations: although normalisation can be proved, the standard proof of Prawitz (Natural deduction. A proof Theoretical ...
Natural Deduction for Full S5 Modal Logic with Weak Normalization
Natural deduction systems for classical, intuitionistic and modal logics were deeply investigated by Prawitz [Prawitz, D., ''Natural Deduction: A Proof-theoretical Study'', Stockholm Studies in Philosophy 3, Almqvist and Wiksell, Stockholm, 1965] from a ...
Monotonic and nonmonotonic gentzen deduction systems for L3-valued propositional logic
AbstractA sequent is a pair (Γ, Δ), which is true under an assignment if either some formula in Γ is false, or some formula in Δ is true. In L3-valued propositional logic, a multisequent is a triple Δ|Θ|Γ, which is true under an assignment if either some ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 10 September 2007
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 12 Dec 2024
Other Metrics
Citations
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in