Verifying Tight Logic Programs with anthem and Vampire

• URL: http://arxiv.org/abs/2008.02025v6
• Date: Mon, 1 May 2023 17:19:20 GMT
• Title: Verifying Tight Logic Programs with anthem and Vampire
• Authors: Jorge Fandinno, Vladimir Lifschitz, Patrick L\"uhne and Torsten Schaub
• Abstract summary: 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. We study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools.
• Score: 7.804960968120875
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• Sequential decomposition of propositional logic programs [0.0]
  This paper studies the sequential decomposition of programs by studying Green's relations between programs. In a broader sense, this paper is a further step towards an algebraic theory of logic programming.
  arXiv  Detail & Related papers  (2023-02-21T16:14:57Z)
• Hybrid Probabilistic Logic Programming: Inference and Learning [1.14219428942199]
  This thesis focuses on advancing probabilistic logic programming (PLP), which combines probability theory for uncertainty and logic programming for relations. The first contribution is the introduction of context-specific likelihood weighting (CS-LW), a new sampling algorithm that exploits context-specific independencies for computational gains. Next, a new hybrid PLP, DC#, is introduced, which integrates the syntax of Distributional Clauses with Bayesian logic programs and represents three types of independencies. The scalable inference algorithm FO-CS-LW is introduced for DC#.
  arXiv  Detail & Related papers  (2023-02-01T15:07:36Z)
• Hierarchical Programmatic Reinforcement Learning via Learning to Compose Programs [58.94569213396991]
  We propose a hierarchical programmatic reinforcement learning framework to produce program policies. By learning to compose programs, our proposed framework can produce program policies that describe out-of-distributionally complex behaviors. The experimental results in the Karel domain show that our proposed framework outperforms baselines.
  arXiv  Detail & Related papers  (2023-01-30T14:50:46Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  We introduce the methodology of Faithfulness-through-Counterfactuals. It generates a counterfactual hypothesis based on the logical predicates expressed in the explanation. It then evaluates if the model's prediction on the counterfactual is consistent with that expressed logic.
  arXiv  Detail & Related papers  (2022-05-25T03:40:59Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Verification of Locally Tight Programs [8.005641341294732]
  Program completion is a translation from the language of logic programs into the language of first-order theories. We show that the tightness condition in this theorem can be replaced by a less restrictive "local tightness" requirement. We conclude that the proof assistant anthem-p2p can be used to verify equivalence between locally tight programs.
  arXiv  Detail & Related papers  (2022-04-18T23:22:54Z)
• Planning with Incomplete Information in Quantified Answer Set Programming [1.3501640559999886]
  We present a general approach to planning with incomplete information in Answer Set Programming (ASP) We represent planning problems using a simple formalism where logic programs describe the transition function between states. We present a translation-based QASP solver that converts quantified logic programs into QBFs and then executes a QBF solver.
  arXiv  Detail & Related papers  (2021-08-13T21:24:47Z)
• Enforcing Consistency in Weakly Supervised Semantic Parsing [68.2211621631765]
  We explore the use of consistency between the output programs for related inputs to reduce the impact of spurious programs. We find that a more consistent formalism leads to improved model performance even without consistency-based training.
  arXiv  Detail & Related papers  (2021-07-13T03:48:04Z)
• Latent Execution for Neural Program Synthesis Beyond Domain-Specific Languages [97.58968222942173]
  We take the first step to synthesize C programs from input-output examples. In particular, we propose La Synth, which learns the latent representation to approximate the execution of partially generated programs. We show that training on these synthesized programs further improves the prediction performance for both Karel and C program synthesis.
  arXiv  Detail & Related papers  (2021-06-29T02:21:32Z)
• Latent Programmer: Discrete Latent Codes for Program Synthesis [56.37993487589351]
  In many sequence learning tasks, such as program synthesis and document summarization, a key problem is searching over a large space of possible output sequences. We propose to learn representations of the outputs that are specifically meant for search: rich enough to specify the desired output but compact enough to make search more efficient. We introduce the emphLatent Programmer, a program synthesis method that first predicts a discrete latent code from input/output examples, and then generates the program in the target language.
  arXiv  Detail & Related papers  (2020-12-01T10:11:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.