4 papers
Anthem 2.0: Automated Reasoning for Answer Set Programming
Jorge Fandinno, Christoph Glinzer, Zachary Hansen +5
Anthem 2.0 is a tool to aid in the verification of logic programs written in an expressive fragment of Clingo's input language named mini-gringo, which includes arithmetic operatio…
Ordered Completion for Non-Locally Tight mini-gringo Programs
Jan Heuer
Completion is a well-known transformation that captures the stable model semantics of logic programs by turning a program into a set of first-order definitions. Stable models are m…
Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
Jan Heuer, Christoph Wernhard
We show a projective Beth definability theorem for logic programs under the stable model semantics: For given programs and and vocabulary (set of predicates) the existe…
Automated Verification of Equivalence Properties in Advanced Logic Programs -- Bachelor Thesis
Jan Heuer
With the increase in industrial applications using Answer Set Programming, the need for formal verification tools, particularly for critical applications, has also increased. Durin…