Automated Verification of Equivalence Properties in Advanced Logic Programs -- Bachelor Thesis

• URL: http://arxiv.org/abs/2310.19806v4
• Date: Wed, 17 Jul 2024 10:23:59 GMT
• Title: Automated Verification of Equivalence Properties in Advanced Logic Programs -- Bachelor Thesis
• Authors: Jan Heuer,
• Abstract summary: 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.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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 would be desirable to have a tool which can automatically verify whether an optimised subprogram can replace the original subprogram. Formally this corresponds to the problem of verifying the strong equivalence of two programs. 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. With the current version of anthem, only the strong equivalence of positive programs with a restricted input language can be verified. This is a result of the translation $\tau^*$ implemented in anthem that produces formulas in the logic of here-and-there, which coincides with classical logic only for positive programs. This thesis extends anthem in order to overcome these limitations. First, the transformation $\sigma^*$ is presented, which transforms formulas from the logic of here-and-there to classical logic. A theorem formalises how $\sigma^*$ can be used to express equivalence in the logic of here-and-there in classical logic. Second, the translation $\tau^*$ is extended to programs containing pools. Another theorem shows how $\sigma^*$ can be combined with $\tau^*$ to express the strong equivalence of two programs in classical logic. With $\sigma^*$ and the extended $\tau^*$, it is possible to express the strong equivalence of logic programs containing negation, simple choices, and pools. Both the extended $\tau^*$ and $\sigma^*$ are implemented in a new version of anthem. Several examples of logic programs containing pools, negation, and simple choice rules, which the new version of anthem can translate to classical logic, are presented. Some a...

Related papers

• Faithful Logical Reasoning via Symbolic Chain-of-Thought [39.94884827166363]
  We propose SymbCoT, a framework that integrates symbolic expressions and logic rules with Chain-of-Thought prompting. We show that SymbCoT shows striking improvements over the CoT method consistently. This is the first to combine symbolic expressions and rules into CoT for logical reasoning with LLMs.
  arXiv  Detail & Related papers  (2024-05-28T16:55:33Z)
• 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)
• Empower Nested Boolean Logic via Self-Supervised Curriculum Learning [67.46052028752327]
  We find that any pre-trained language models even including large language models only behave like a random selector in the face of multi-nested logic. To empower language models with this fundamental capability, this paper proposes a new self-supervised learning method textitCurriculum Logical Reasoning (textscClr)
  arXiv  Detail & Related papers  (2023-10-09T06:54:02Z)
• Normative Conditional Reasoning as a Fragment of HOL [0.0]
  We discuss the mechanization of (preference-based) conditional normative reasoning. Our focus is on Aqvist's system E for conditional obligation, and its extensions. We consider two possible uses of the framework.
  arXiv  Detail & Related papers  (2023-08-21T12:47:30Z)
• Strong Equivalence of Logic Programs with Ordered Disjunction: a Logical Perspective [1.160208922584163]
  Logic Programs with Ordered Disjunction (LPODs) extend classical logic programs with the capability of expressing preferential disjunctions. In this paper we obtain a purely logical characterization of strong equivalence of LPODs as logical equivalence in a four-valued logic. We provide a new proof of the coNP-completeness of strong equivalence for LPODs, which has an interest in its own right since it relies on the special structure of such programs.
  arXiv  Detail & Related papers  (2022-05-10T13:33:32Z)
• 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)
• An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning [91.3755431537592]
  The logic embedding tool provides a procedural encoding for non-classical reasoning problems into classical higher-order logic. It can support an increasing number of different non-classical logics as reasoning targets.
  arXiv  Detail & Related papers  (2022-03-23T12:08:51Z)
• A Logic-Based Framework for Natural Language Inference in Dutch [1.0178220223515955]
  We present a framework for deriving relations between Dutch sentence pairs. The proposed framework relies on logic-based reasoning to produce inspectable proofs leading up to inference labels. We evaluate the reasoning pipeline on the recently created Dutch natural language inference dataset.
  arXiv  Detail & Related papers  (2021-10-07T10:34:46Z)
• Logic-Driven Context Extension and Data Augmentation for Logical Reasoning of Text [65.24325614642223]
  We propose to understand logical symbols and expressions in the text to arrive at the answer. Based on such logical information, we put forward a context extension framework and a data augmentation algorithm. Our method achieves the state-of-the-art performance, and both logic-driven context extension framework and data augmentation algorithm can help improve the accuracy.
  arXiv  Detail & Related papers  (2021-05-08T10:09:36Z)
• Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
  We introduce refutationally complete superposition calculi for intentional and extensional clausal $lambda$-free higher-order logic. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the $lambda$-free higher-order lexicographic path and Knuth-Bendix orders.
  arXiv  Detail & Related papers  (2020-05-05T12:10:21Z)

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.