Natural deduction as higher-order resolution
From MaRDI portal
Publication:4720797
DOI10.1016/0743-1066(86)90015-4zbMath0613.68035WikidataQ55894613 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
types; Horn clauses; natural deduction; Resolution; interactive theorem prover; higher- order unification; Huet's search procedure; LCF theorem provers; Logic of Computable Functions; Martin-Löf constructive type theory
03B35: Mechanization of proofs and logical operations
Related Items
Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology, Using typed lambda calculus to implement formal systems on a machine, 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, Constructing recursion operators in intuitionistic type theory, A unification algorithm for second-order monadic terms, Unification under a mixed prefix, Program development schemata as derived rules, The foundation of a generic theorem prover, Higher-order unification revisited: Complete sets of transformations, A type-theoretic approach to program development, Uniform proofs as a foundation for logic programming, The Isabelle Framework, Unnamed Item
