Verifying Tight Logic Programs with anthem and Vampire
This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas. Under consideration for acceptance in TPLP.
Code (0)
등록된 구현이 없습니다.
Tasks
LEMMASimilar Papers 제목 키워드 기반
Automated Verification of Equivalence Properties in Advanced Logic Programs -- Bachelor Thesis
With the increase in industrial applications using Answer Set Programming, the need for formal verification tools, particularly for critical applications, has also increased. During the program optimisation process, it w…
NegationTranslationVerification of Locally Tight Programs
Program completion is a translation from the language of logic programs into the language of first-order theories. Its original definition has been extended to programs that include integer arithmetic, accept input, and …
Tea Chrysanthemum Detection under Unstructured Environments Using the TC-YOLO Model
Tea chrysanthemum detection at its flowering stage is one of the key components for selective chrysanthemum harvesting robot development. However, it is a challenge to detect flowering chrysanthemums under unstructured f…
GPUVampire With a Brain Is a Good ITP Hammer
Vampire has been for a long time the strongest first-order automatic theorem prover, widely used for hammer-style proof automation in ITPs such as Mizar, Isabelle, HOL, and Coq. In this work, we considerably improve the …
Analyzing Musical Characteristics of National Anthems in Relation to Global Indices
Music plays a huge part in shaping peoples' psychology and behavioral patterns. This paper investigates the connection between national anthems and different global indices with computational music analysis and statistic…
Relation