Operational semantics of resolution and productivity in Horn clause logic

DOI10.1007/s00165-016-0403-1zbMath1362.68048arXiv1604.04114OpenAlexW2507158969WikidataQ59614631 ScholiaQ59614631MaRDI QIDQ2628299

Peng Fu, Ekaterina Komendantskaya

Publication date: 1 June 2017

Published in: Formal Aspects of Computing (Search for Journal in Brave)

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

zbMATH Keywords

productivityterminationlogic programmingtyped lambda calculusreduction systemsstructural resolution

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (9)

Transforming orthogonal inductive definition sets into confluent term rewrite systems ⋮ Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis ⋮ First-order Answer Set Programming as Constructive Proof Search ⋮ On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs ⋮ Productive corecursion in logic programming ⋮ The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them ⋮ A coinductive approach to proof search through typed lambda-calculi ⋮ Logic programming: laxness and saturation ⋮ \texttt{slepice}: towards a verified implementation of type theory in type theory

Uses Software

• CoALP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination of term rewriting using dependency pairs
• A productivity checker for logic programming
• Uniform proofs as a foundation for logic programming
• Proof Relevant Corecursive Resolution
• Coalgebraic Derivations in Logic Programming
• Scrap your boilerplate with class
• Coinductive Logic Programming and Its Applications
• Term Rewriting and All That
• Mechanizing metatheory in a logical framework
• Co-Logic Programming: Extending Logic Programming with Coinduction
• Coalgebraic logic programming: from Semantics to Implementation

This page was built for publication: Operational semantics of resolution and productivity in Horn clause logic