Modules and Logic Programming
Christophe Fouquere, Virgile Mogbil
TL;DR
This paper explores conditions and correctness criteria for the concurrent construction of proof-nets in logic programming, focusing on validity, acyclicity, and connectability for incremental verification.
Contribution
It introduces specific correctness criteria for concurrent proof-net construction, extending from closed to open modules with incremental verification methods.
Findings
Defined correctness criteria for proof-net validity
Extended criteria to open modules for incremental validation
Provided conditions for acyclicity and connectability
Abstract
We study conditions for a concurrent construction of proof-nets in the framework developed by Andreoli in recent papers. We define specific correctness criteria for that purpose. We first study closed modules (i.e. validity of the execution of a logic program), then extend the criterion to open modules (i.e. validity during the execution) distinguishing criteria for acyclicity and connectability in order to allow incremental verification.
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
TopicsFormal Methods in Verification · Logic, programming, and type systems · Logic, Reasoning, and Knowledge