2026/07/20 by Marco Pérez, Pedro López-García, Jose F. Morales +2
Computer Science · #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Formal Methods in Verification
paper · pdf · doi:10.4204/eptcs.450.18
interpretation-based verification is a central component of the Ciao Prolog system, enabling expressive specifications of properties of programs, predicates, and execution states.Independently, the LPTP (Logic Programming Theorem Proving) framework offers a first-order logical formalism for expressing and proving properties of predicates.In this paper, we address a fundamental issue in relating these two frameworks: studying the translation of Ciao assertions into LPTP formulae and identifying a partial correspondence between assertion-based and logic-based specifications.We introduce a systematic translation scheme, characterize assertion classes according to their logical encodability, and propose approximation strategies and auxiliary constructs for non-translatable cases, and finally analyze the resulting soundness and completeness trade-offs.We argue that our proposal enables a tight integration of Ciao 's assertion checking with LPTP-based deductive verification, thereby leveraging their complementary capabilities.