On systematic construction of correct logic programs

• URL: http://arxiv.org/abs/2508.16782v1
• Date: Fri, 22 Aug 2025 20:27:21 GMT
• Title: On systematic construction of correct logic programs
• Authors: Włodzimierz Drabent,
• Abstract summary: This paper presents an approach to systematically construct provably correct and semi-complete logic programs.<n>The proposed method is simple, and can be used (maybe informally) in actual everyday programming.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Partial correctness of imperative or functional programming divides in logic programming into two notions. Correctness means that all answers of the program are compatible with the specification. Completeness means that the program produces all the answers required by the specifications. We also consider semi-completeness -- completeness for those queries for which the program does not diverge. This paper presents an approach to systematically construct provably correct and semi-complete logic programs, for a given specification. Normal programs are considered, under Kunen's 3-valued completion semantics (of negation as finite failure) and the well-founded semantics (of negation as possibly infinite failure). The approach is declarative, it abstracts from details of operational semantics, like e.g.\ the form of the selected literals (``procedure calls'') during the computation. The proposed method is simple, and can be used (maybe informally) in actual everyday programming.

Related papers

• SM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic [3.9335611819745355]
  Conditional literals behave as nested implications within bodies of logic rules.<n>We propose a semantics for logic programs with conditional literals and arithmetic based on the SM operator.
  arXiv  Detail & Related papers  (2025-11-03T17:03:29Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  Modern language models (LMs) exhibit strong deductive reasoning capabilities, yet standard evaluations emphasize correctness while overlooking a key aspect of human-like reasoning: efficiency.<n>We propose a framework for assessing LM reasoning efficiency through the lens of logic programming.
  arXiv  Detail & Related papers  (2025-10-29T15:30:31Z)
• A Reduction of Input/Output Logics to SAT [51.82266520875928]
  Deontic logics are formalisms for reasoning over norms, obligations, permissions and prohibitions.<n>In this paper, an automation approach for I/O logics is presented that makes use of suitable reductions to propositional satisfiability problems.
  arXiv  Detail & Related papers  (2025-08-22T09:22:26Z)
• Relating Answer Set Programming and Many-sorted Logics for Formal Verification [1.223779595809275]
  My research agenda has been focused on addressing three issues with the intention of making ASP verification an accessible, routine task.<n>I have investigated alternative semantics for ASP based on translations into the logic of here-and-there and many-sorted first-order logic.<n>These semantics promote a modular understanding of logic programs, bypass grounding, and enable us to use automated theorem provers to automatically verify properties of programs.
  arXiv  Detail & Related papers  (2025-02-13T11:52:40Z)
• 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)
• On Feasibility of Declarative Diagnosis [0.0]
  We argue that useful ways of declarative diagnosis of logic programs exist, and should be usable in actual programming. This paper discusses their possibly main weaknesses and shows how to overcome them.
  arXiv  Detail & Related papers  (2023-08-30T08:56:19Z)
• 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)
• 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)
• Foundations of Reasoning with Uncertainty via Real-valued Logics [70.43924776071616]
  We give a sound and strongly complete axiomatization that can be parametrized to cover essentially every real-valued logic. Our class of sentences are very rich, and each describes a set of possible real values for a collection of formulas of the real-valued logic.
  arXiv  Detail & Related papers  (2020-08-06T02:13:11Z)

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.