Typed SLD-resolution: dynamic typing for logic programming

DOI10.1007/978-3-031-16767-6_7MaRDI QIDQ6103019zbMATHFDO

Authors

Publication date 2 June 2023

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2208.00192

zbMATH Keywords

typeslogic programmingoperational semantics

Mathematics Subject Classification ID

Logic programming (68N17) Semantics in the theory of computing (68Q55)

Abstract: The semantic foundations for logic programming are usually separated into two different approaches. The operational semantics, which uses SLD-resolution, the proof method that computes answers in logic programming, and the declarative semantics, which sees logic programs as formulas and its semantics as models. Here, we define a new operational semantics called TSLD-resolution, which stands for Typed SLD-resolution, where we include a value "wrong", that corresponds to the detection of a type error at run-time. For this we define a new typed unification algorithm. Finally we prove the correctness of TSLD-resolution with respect to a typed declarative semantics.

Recommendations

• scientific article; zbMATH DE number 516997
• A type-theoretic approach to resolution
• A type system for logic programs
• Efficient run-time type checking of typed logic programs
• On types and type consistency in logic programming (Diss., FernUniv. Hagen, 1999)

Cites work

• scientific article; zbMATH DE number 1692902 (Why is no real title available?)
• scientific article; zbMATH DE number 3872640 (Why is no real title available?)
• scientific article; zbMATH DE number 867332 (Why is no real title available?)
• scientific article; zbMATH DE number 7453101 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A polymorphic type system for Prolog
• A theory of type polymorphism in programming
• An Efficient Unification Algorithm
• Data type inference for logic programming
• Efficient run-time type checking of typed logic programs
• From Monomorphic to Polymorphic Well-Typings and Beyond
• Off-topic: a new interpretation of weak Kleene logic
• On a three-valued logical calculus and its application to the analysis of the paradoxes of the classical extended functional calculus
• The Semantics of Predicate Logic as a Programming Language
• The YAP prolog system
• Towards Typed Prolog
• Using parametric set constraints for locating errors in CLP programs
• Well-Typed Programs Can’t Be Blamed

Cited in

(3)

• A typed resolution principle for deduction with conditional typing theory
• A type-theoretic approach to resolution
• scientific article; zbMATH DE number 516997 (Why is no real title available?)

This page was built for publication: Typed SLD-resolution: dynamic typing for logic programming

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