Verification of Locally Tight Programs

• URL: http://arxiv.org/abs/2204.10789v3
• Date: Sun, 24 Dec 2023 19:38:15 GMT
• Title: Verification of Locally Tight Programs
• Authors: Jorge Fandinno, Vladimir Lifschitz, Nathan Temple
• Abstract summary: 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.
• Score: 8.005641341294732
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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 distinguish between output predicates and auxiliary predicates. For tight programs, that generalization of completion is known to match the stable model semantics, which is the basis of answer set programming. We show that the tightness condition in this theorem can be replaced by a less restrictive "local tightness" requirement. From this fact we conclude that the proof assistant anthem-p2p can be used to verify equivalence between locally tight programs. Under consideration for publication in Theory and Practice of Logic Programming

Related papers

• Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
  We propose Chain of Code, a simple yet surprisingly effective extension that improves LM code-driven reasoning. The key idea is to encourage LMs to format semantic sub-tasks in a program as flexible pseudocode that the interpreter can explicitly catch.
  arXiv  Detail & Related papers  (2023-12-07T17:51:43Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  Logical reasoning is an important task for artificial intelligence with potential impacts on science, mathematics, and society. In this work, we reformulating such tasks as modular neurosymbolic programming, which we call LINC. We observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate.
  arXiv  Detail & Related papers  (2023-10-23T17:58:40Z)
• Automated Verification of Equivalence Properties in Advanced Logic Programs -- Bachelor Thesis [0.0]
  It would be desirable to have a tool which can automatically verify whether an optimised subprogram can replace the original subprogram. In order to do so, the translation tool anthem was developed. It can be used in conjunction with an automated theorem prover for classical logic to verify that two programs are strongly equivalent.
  arXiv  Detail & Related papers  (2023-10-11T08:19:22Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  Learned transpilation offers an alternative to manual re-writing and engineering efforts. Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness. Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence.
  arXiv  Detail & Related papers  (2023-09-25T15:42:18Z)
• Natural Language to Code Translation with Execution [82.52142893010563]
  Execution result--minimum Bayes risk decoding for program selection. We show that it improves the few-shot performance of pretrained code models on natural-language-to-code tasks.
  arXiv  Detail & Related papers  (2022-04-25T06:06:08Z)
• Thirty years of Epistemic Specifications [8.339560855135575]
  We extend disjunctive logic programs under the stable model semantics with modal constructs called subjective literals. Using subjective literals, it is possible to check whether a regular literal is true in every or some stable models of the program. Several attempts for capturing the intuitions underlying the language by means of a formal semantics were given.
  arXiv  Detail & Related papers  (2021-08-17T15:03:10Z)
• Non-ground Abductive Logic Programming with Probabilistic Integrity Constraints [2.624902795082451]
  In this paper, we consider a richer logic language, coping with probabilistic abduction with variables. We first present the overall abductive language, and its semantics according to the Distribution Semantics. We then introduce a proof procedure, obtained by extending one previously presented, and prove its soundness and completeness.
  arXiv  Detail & Related papers  (2021-08-06T10:22:12Z)
• 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 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)
• Verifying Tight Logic Programs with anthem and Vampire [7.804960968120875]
  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.
  arXiv  Detail & Related papers  (2020-08-05T10:01:33Z)

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.