Pages that link to "Item:Q4720797"

The following pages link to Natural deduction as higher-order resolution (Q4720797):

Displaying 35 items.

• On the use of naturality in algorithmic resolution (Q615863) (← links)
• Using typed lambda calculus to implement formal systems on a machine (Q688571) (← links)
• Synthesis of rewrite programs by higher-order and semantic unification (Q749216) (← links)
• Simple second-order languages for which unification is undecidable (Q807609) (← links)
• Verifying termination and reduction properties about higher-order logic programs (Q850496) (← links)
• Term rewriting and beyond -- theorem proving in Isabelle (Q909488) (← links)
• Constructive system for automatic program synthesis (Q912589) (← links)
• Natural deduction and arbitrary objects (Q1061731) (← links)
• Constructing recursion operators in intuitionistic type theory (Q1094421) (← links)
• A unification algorithm for second-order monadic terms (Q1109019) (← links)
• Unification under a mixed prefix (Q1201348) (← links)
• Proof-functional connectives and realizability (Q1330311) (← links)
• Program development schemata as derived rules (Q1583853) (← links)
• The foundation of a generic theorem prover (Q1823013) (← links)
• Higher-order unification revisited: Complete sets of transformations (Q1823936) (← links)
• Automated proof construction in type theory using resolution (Q1868508) (← links)
• The locally nameless representation (Q1945914) (← links)
• Formalization of the Poincaré disc model of hyperbolic geometry (Q2031408) (← links)
• A type-theoretic approach to program development (Q2277827) (← links)
• From LCF to Isabelle/HOL (Q2280211) (← links)
• Mechanized metatheory revisited (Q2323447) (← links)
• Uniform proofs as a foundation for logic programming (Q2640596) (← links)
• The Isabelle Framework (Q3543647) (← links)
• Lessons learned from LCF: A Survey of Natural Deduction Proofs (Q3696549) (← links)
• Indexed categories for program development (Q3986546) (← links)
• (Q4438235) (← links)
• Computational logic: its origins and applications (Q4559535) (← links)
• Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology (Q4827602) (← links)
• Some normalization properties of martin-löf's type theory, and applications (Q5096234) (← links)
• The practice of logical frameworks (Q5878905) (← links)
• Higher-order unification, polymorphism, and subsorts (Q5881304) (← links)
• Investigations into proof-search in a system of first-order dependent function types (Q6488534) (← links)
• Higher order E-unification (Q6488561) (← links)
• Programming by example and proving by example using higher-order unification (Q6488562) (← links)
• Higher-order annotated terms for proof search (Q6567727) (← links)