Natural deduction as higher-order resolution

DOI10.1016/0743-1066(86)90015-4zbMath0613.68035DBLPjournals/jlp/Paulson86OpenAlexW2070577487WikidataQ55894613 ScholiaQ55894613MaRDI QIDQ4720797

Lawrence Charles 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

typesHorn clausesnatural deductionResolutioninteractive theorem proverhigher- order unificationHuet's search procedureLCF theorem proversLogic of Computable FunctionsMartin-Löf constructive type theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (26)

Higher-order unification, polymorphism, and subsorts ⋮ Constructing recursion operators in intuitionistic type theory ⋮ Verifying termination and reduction properties about higher-order logic programs ⋮ Uniform proofs as a foundation for logic programming ⋮ A unification algorithm for second-order monadic terms ⋮ 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 ⋮ Formalising Mathematics in Simple Type Theory ⋮ The locally nameless representation ⋮ Term rewriting and beyond -- theorem proving in Isabelle ⋮ Constructive system for automatic program synthesis ⋮ The Isabelle Framework ⋮ Using typed lambda calculus to implement formal systems on a machine ⋮ Unification under a mixed prefix ⋮ A type-theoretic approach to program development ⋮ Unnamed Item ⋮ From LCF to Isabelle/HOL ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ Synthesis of rewrite programs by higher-order and semantic unification ⋮ The foundation of a generic theorem prover ⋮ Higher-order unification revisited: Complete sets of transformations ⋮ Mechanized metatheory revisited ⋮ Program development schemata as derived rules ⋮ Simple second-order languages for which unification is undecidable ⋮ The practice of logical frameworks

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