A semantics for \(\lambda \)Prolog

DOI10.1016/0304-3975(93)00130-WzbMath0874.68181OpenAlexW2022937548MaRDI QIDQ1349686

D. A. Wolfram

Publication date: 27 February 1997

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(93)00130-w

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Related Items (2)

Kripke semantics for higher-order type theory applied to constraint logic programming languages ⋮ Abstract deduction and inferential models for type theory

Uses Software

• ETPS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Kripke-style models for typed lambda calculus
• A unification algorithm for typed \(\overline\lambda\)-calculus
• A proof of cut-elimination theorem in simple type-theory
• Uniform proofs as a foundation for logic programming
• Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
• Higher-order Horn clauses
• Syntactical and semantical properties of simple type theory
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• The Semantics of Predicate Logic as a Programming Language
• Hauptsatz for higher order logic
• Resolution in type theory
• General models and extensionality
• Completeness in the theory of types
• Proof theory

This page was built for publication: A semantics for \(\lambda \)Prolog