Horn clause programs with polymorphic types: Semantics and resolution

DOI10.1016/0304-3975(90)90107-SMaRDI QIDQ1177936zbMATH OpenOpenAlexFDO

Authors Michael Hanus

Publication date 26 June 1992

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

Full work available at URL https://doi.org/10.1016/0304-3975(90)90107-s

zbMATH Keywords

polymorphic typesresolutionsemantics

Mathematics Subject Classification ID

Logic programming (68N17)

Review text

A Horn clause logic where functions and predicates are declared with polymorphic types is presented. The semantics models for polymorphic Horn clause programs are defined. Deduction and resolution methods for typed logic programs are presented. For several classes of programs, optimizations of the resolution procedure are given. It is shown that higher-order programming techniques can be applied in the framework.

Recommendations

• Logic programs with polymorphic types: A condition for static type checking
• Higher-order Horn clauses
• scientific article; zbMATH DE number 44623
• A bottom-up polymorphic type inference in logic programming
• Operational semantics of resolution and productivity in Horn clause logic

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A polymorphic type system for Prolog
• A type system for logic programs
• A unification algorithm for typed -calculus
• An Efficient Unification Algorithm
• Contributions to the Theory of Logic Programming
• Horn clause programs with polymorphic types: Semantics and resolution
• scientific article; zbMATH DE number 4176425 (Why is no real title available?)
• scientific article; zbMATH DE number 3888893 (Why is no real title available?)
• scientific article; zbMATH DE number 3872640 (Why is no real title available?)
• scientific article; zbMATH DE number 3945331 (Why is no real title available?)
• scientific article; zbMATH DE number 3988745 (Why is no real title available?)
• scientific article; zbMATH DE number 3784848 (Why is no real title available?)
• scientific article; zbMATH DE number 193539 (Why is no real title available?)
• scientific article; zbMATH DE number 3992919 (Why is no real title available?)
• Linear unification
• Login: a logic programming language with built-in inheritance
• On specifications, theories, and models with higher types
• The Semantics of Predicate Logic as a Programming Language
• The undecidability of the second-order unification problem

Cited in

(13)

• Horn clause programs with polymorphic types: Semantics and resolution
• A typed functional extension of logic programming
• Specification and correctness proof of a WAM extension with abstract type constraints
• Refinement of a typed WAM extension by polymorphic order-sorted types
• Operational semantics of resolution and productivity in Horn clause logic
• Towards a Type Discipline for Answer Set Programming
• scientific article; zbMATH DE number 44623 (Why is no real title available?)
• scientific article; zbMATH DE number 1942464 (Why is no real title available?)
• Horn clauses as an intermediate representation for program analysis and transformation
• Prolog's control constructs in a functional setting -- axioms and implementation
• A type-theoretic approach to resolution
• Logic programs with polymorphic types: A condition for static type checking
• Relating the implementation techniques of functional and functional logic languages

This page was built for publication: Horn clause programs with polymorphic types: Semantics and resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1177936)