Typed SLD-resolution: dynamic typing for logic programming

DOI10.1007/978-3-031-16767-6_7zbMATH Open1522.68098arXiv2208.00192MaRDI QIDQ6103019FDOQ6103019

Authors:

Publication date: 2 June 2023

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

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.

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

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)

zbMATH Keywords

typeslogic programmingoperational semantics

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (3)

• A typed resolution principle for deduction with conditional typing theory
• A type-theoretic approach to resolution
• Title not available (Why is that?)

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)