Proof Relevant Corecursive Resolution

DOI10.1007/978-3-319-29604-3_9zbMath1475.68054arXiv1511.09394OpenAlexW2277609624MaRDI QIDQ2798268

Andrew Pond, Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers

Publication date: 4 April 2016

Published in: Functional and Logic Programming (Search for Journal in Brave)

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

zbMATH Keywords

resolutioncorecursionHorn clause logiccoinductive proofsHaskell-type class inference

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Logic programming (68N17)

Related Items

Operational semantics of resolution and productivity in Horn clause logic, Productive corecursion in logic programming, Into the Infinite - Theory Exploration for Coinduction, Unnamed Item, 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, Category Theoretic Semantics for Theorem Proving in Logic Programming: Embracing the Laxness

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A principled approach to programming with nested types in Haskell
• Termination of rewriting
• Uniform proofs as a foundation for logic programming
• Scrap your boilerplate with class
• Horn Clause Solvers for Program Verification
• Idealized coinductive type systems for imperative object-oriented programs
• On the Foundations of Corecursion
• Understanding functional dependencies via constraint handling rules
• Non-Looping String Rewriting
• Qualified Types
• Derivable Type Classes
• Co-Logic Programming: Extending Logic Programming with Coinduction
• A Type-Theoretic Approach to Resolution