Natural deduction as higher-order resolution

DOI10.1016/0743-1066(86)90015-4MaRDI QIDQ4720797zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Lawrence C. Paulson

Publication date 1986

Published in The Journal of Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0743-1066(86)90015-4

zbMATH Keywords

higher- order unificationHorn clausesHuet's search procedureinteractive theorem proverLCF theorem proversLogic of Computable FunctionsMartin-Löf constructive type theorynatural deductionResolutiontypes

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 2015404
• Naturalizing natural deduction
• A natural extension of natural deduction
• Natural deduction in a paracomplete setting
• Natural deduction in normal modal logic
• Natural deduction for non-classical logics
• Natural deduction
• Natural deduction for paraconsistent logic
• scientific article; zbMATH DE number 575583
• Natural Deduction for Hybrid Logic

Cited in

(39)

• Natural deduction and arbitrary objects
• Constructing recursion operators in intuitionistic type theory
• A unification algorithm for second-order monadic terms
• Unification under a mixed prefix
• Proof-functional connectives and realizability
• Program development schemata as derived rules
• The foundation of a generic theorem prover
• Higher-order unification revisited: Complete sets of transformations
• Automated proof construction in type theory using resolution
• The locally nameless representation
• Formalization of the Poincaré disc model of hyperbolic geometry
• A type-theoretic approach to program development
• From LCF to Isabelle/HOL
• Mechanized metatheory revisited
• Uniform proofs as a foundation for logic programming
• scientific article; zbMATH DE number 1614692 (Why is no real title available?)
• The Isabelle Framework
• Lessons learned from LCF: A Survey of Natural Deduction Proofs
• scientific article; zbMATH DE number 29052 (Why is no real title available?)
• scientific article; zbMATH DE number 2015404 (Why is no real title available?)
• Computational logic: its origins and applications
• Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
• Some normalization properties of Martin-Löf's type theory, and applications
• The practice of logical frameworks
• Higher-order unification, polymorphism, and subsorts
• Formalising Mathematics in Simple Type Theory
• On the use of naturality in algorithmic resolution
• Investigations into proof-search in a system of first-order dependent function types
• Higher order E-unification
• Programming by example and proving by example using higher-order unification
• Higher-order annotated terms for proof search
• Using typed lambda calculus to implement formal systems on a machine
• Model checking of distributed algorithms using synchronous programs
• Formal verification of BDI agents
• Synthesis of rewrite programs by higher-order and semantic unification
• Simple second-order languages for which unification is undecidable
• Verifying termination and reduction properties about higher-order logic programs
• Term rewriting and beyond -- theorem proving in Isabelle
• Constructive system for automatic program synthesis

This page was built for publication: Natural deduction as higher-order resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4720797)