Modular Answer Set Programming as a Formal Specification Language

• URL: http://arxiv.org/abs/2008.02015v2
• Date: Fri, 7 Aug 2020 09:40:40 GMT
• Title: Modular Answer Set Programming as a Formal Specification Language
• Authors: Pedro Cabalar, Jorge Fandinno and Yuliya Lierler
• Abstract summary: We study the problem of formal verification for Answer Set Programming (ASP) We obtain a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance.
• Score: 8.823761706435814
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. Under consideration for acceptance in TPLP.

Related papers

• Combining Logic with Large Language Models for Automatic Debugging and Repair of ASP Programs [1.0650780147044159]
  FormHe is a tool that combines logic-based techniques and Large Language Models to identify and correct issues in Answer Set Programming submissions. We show that FormHe accurately detects faults in 94% of cases and successfully repairs 58% of incorrect submissions.
  arXiv  Detail & Related papers  (2024-10-28T12:30:48Z)
• Inductive Predicate Synthesis Modulo Programs (Extended) [1.7372615815088566]
  A growing trend in program analysis is to encode verification conditions within the language of the input program. We propose Inductive Predicate Synthesis Modulo Programs (IPS-MP) which extends high-level languages with minimal synthesis features.
  arXiv  Detail & Related papers  (2024-07-11T12:51:08Z)
• Is Modularity Transferable? A Case Study through the Lens of Knowledge Distillation [59.37775534633868]
  We present an extremely straightforward approach to transferring pre-trained, task-specific PEFT modules between same-family PLMs. We also propose a method that allows the transfer of modules between incompatible PLMs without any change in the inference complexity.
  arXiv  Detail & Related papers  (2024-03-27T17:50:00Z)
• How Proficient Are Large Language Models in Formal Languages? An In-Depth Insight for Knowledge Base Question Answering [52.86931192259096]
  Knowledge Base Question Answering (KBQA) aims to answer natural language questions based on facts in knowledge bases. Recent works leverage the capabilities of large language models (LLMs) for logical form generation to improve performance.
  arXiv  Detail & Related papers  (2024-01-11T09:27:50Z)
• SCREWS: A Modular Framework for Reasoning with Revisions [58.698199183147935]
  We present SCREWS, a modular framework for reasoning with revisions. We show that SCREWS unifies several previous approaches under a common framework. We evaluate our framework with state-of-the-art LLMs on a diverse set of reasoning tasks.
  arXiv  Detail & Related papers  (2023-09-20T15:59:54Z)
• Coupling Large Language Models with Logic Programming for Robust and General Reasoning from Text [5.532477732693001]
  We show that a large language model can serve as a highly effective few-shot semantically. It can convert natural language sentences into a logical form that serves as input for answer set programs. We demonstrate that this method achieves state-of-the-art performance on several benchmarks, including bAbI, StepGame, CLUTRR, and gSCAN.
  arXiv  Detail & Related papers  (2023-07-15T03:29:59Z)
• Resolution for Constrained Pseudo-Propositional Logic [0.0]
  This work shows how propositional resolution can be generalized to obtain a resolution proof system for constrained pseudo-propositional logic. Unlike the construction of CNF formulas which are restricted to a finite set of clauses, the extended CPPL does not require the corresponding set to be finite.
  arXiv  Detail & Related papers  (2023-06-11T09:17:24Z)
• Faithful Question Answering with Monte-Carlo Planning [78.02429369951363]
  We propose FAME (FAithful question answering with MontE-carlo planning) to answer questions based on faithful reasoning steps. We formulate the task as a discrete decision-making problem and solve it through the interaction of a reasoning environment and a controller. FAME achieves state-of-the-art performance on the standard benchmark.
  arXiv  Detail & Related papers  (2023-05-04T05:21:36Z)
• 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)
• 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)
• Text Modular Networks: Learning to Decompose Tasks in the Language of Existing Models [61.480085460269514]
  We propose a framework for building interpretable systems that learn to solve complex tasks by decomposing them into simpler ones solvable by existing models. We use this framework to build ModularQA, a system that can answer multi-hop reasoning questions by decomposing them into sub-questions answerable by a neural factoid single-span QA model and a symbolic calculator.
  arXiv  Detail & Related papers  (2020-09-01T23:45:42Z)

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.