A logic programming language with lambda-abstraction, function variables, and simple unification

DOI10.1007/BFb0038698zbMath1502.68070OpenAlexW1542795482MaRDI QIDQ5053011

No author found.

Publication date: 26 November 2022

Published in: Extensions of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bfb0038698

Mathematics Subject Classification ID

Logic in computer science (03B70) Logic programming (68N17) Combinatory logic and lambda calculus (03B40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (20)

Context rewriting ⋮ Higher-Ranked Annotation Polymorphic Dependency Analysis ⋮ Rewriting, and equational unification: the higher-order cases ⋮ A restricted form of higher-order rewriting applied to an HDL semantics ⋮ Problems in rewriting III ⋮ Higher-order superposition for dependent types ⋮ Higher-order families ⋮ Middle-out reasoning for synthesis and induction ⋮ Higher order disunification: Some decidable cases ⋮ Higher order conditional rewriting and narrowing ⋮ Developing developments ⋮ Existential type systems between Church and Curry style (type-free style) ⋮ Constraint handling rules with binders, patterns and generic quantification ⋮ Cut elimination for a logic with induction and co-induction ⋮ A theory of binding structures and applications to rewriting ⋮ Normalisation for higher-order calculi with explicit substitutions ⋮ Inductive-data-type systems ⋮ Representing proof transformations for program optimization ⋮ Decidable higher-order unification problems ⋮ Higher order unification via explicit substitutions

This page was built for publication: A logic programming language with lambda-abstraction, function variables, and simple unification