Structural Resolution for Logic Programming
P. Johann, E. Komendantskaya, V. Komendantskiy
TL;DR
This paper introduces a Three Tier Tree Calculus (3TC) that systematically models proof search in logic programming, leading to a new structural resolution method.
Contribution
The paper presents a novel three-tier tree calculus and a structural resolution approach for logic programming, advancing proof search techniques.
Findings
Defines a systematic three-tier tree calculus (3TC)
Develops a new structural resolution method
Enhances understanding of proof search in logic programming
Abstract
We introduce a Three Tier Tree Calculus (3TC) that defines in a systematic way three tiers of tree structures underlying proof search in logic programming. We use 3TC to define a new -- structural -- version of resolution for logic programming.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification