Verifying Tight Logic Programs with anthem and vampire

DOI10.1017/S1471068420000344zbMath1468.68127arXiv2008.02025MaRDI QIDQ5140011

Torsten Schaub, Vladimir Lifschitz, Jorge Fandinno, Patrick Lühne

Publication date: 13 December 2020

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2008.02025

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17) Basic properties of first-order languages and structures (03C07)

Related Items (5)

Here and There with Arithmetic ⋮ Arguing correctness of ASP programs with aggregates ⋮ Semantics for conditional literals via the SM operator ⋮ Testing in ASP: revisited language and programming environment ⋮ Transforming gringo rules into formulas in a natural way

Uses Software

• VAMPIRE
• TPTP
• Gringo
• anthem

Cites Work

• Stable models and circumscription
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Verifying strong equivalence of programs in the input language of \textsc{gringo}
• Infinitary equilibrium logic and strongly equivalent logic programs
• Connecting First-Order ASP and the Logic FO(ID) through Reducts
• A Translation-based Approach to the Verification of Modular Equivalence
• Program completion in the input language of GRINGO
• Abstract gringo
• Tight logic programs
• Towards Verifying Logic Programs in the Input Language of clingo
• Logic Programming and Nonmonotonic Reasoning

This page was built for publication: Verifying Tight Logic Programs with anthem and vampire