Natural deduction as higher-order resolution
From MaRDI portal
Publication:4720797
DOI10.1016/0743-1066(86)90015-4zbMath0613.68035OpenAlexW2070577487WikidataQ55894613 ScholiaQ55894613MaRDI QIDQ4720797
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
typesHorn clausesnatural deductionResolutioninteractive theorem proverhigher- order unificationHuet's search procedureLCF theorem proversLogic of Computable FunctionsMartin-Löf constructive type theory
Related Items
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
