Modal Logic S5 Satisfiability in Answer Set Programming
- URL: http://arxiv.org/abs/2108.04194v1
- Date: Mon, 9 Aug 2021 17:35:31 GMT
- Title: Modal Logic S5 Satisfiability in Answer Set Programming
- Authors: Mario Alviano, Sotiris Batsakis, George Baryannis
- Abstract summary: We propose to use Answer Set Programming for implementing propositional atoms that are relevant in every world.
The proposed encodings are designed to take advantage of other properties such as entailment relations of subformulas rooted by modal operators.
An empirical assessment of the proposed encodings shows that the reachability relation is very effective and leads to comparable performance to a state-of-the-art S5 solver.
- Score: 8.89493507314525
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Modal logic S5 has attracted significant attention and has led to several
practical applications, owing to its simplified approach to dealing with
nesting modal operators. Efficient implementations for evaluating
satisfiability of S5 formulas commonly rely on Skolemisation to convert them
into propositional logic formulas, essentially by introducing copies of
propositional atoms for each set of interpretations (possible worlds). This
approach is simple, but often results into large formulas that are too
difficult to process, and therefore more parsimonious constructions are
required. In this work, we propose to use Answer Set Programming for
implementing such constructions, and in particular for identifying the
propositional atoms that are relevant in every world by means of a reachability
relation. The proposed encodings are designed to take advantage of other
properties such as entailment relations of subformulas rooted by modal
operators. An empirical assessment of the proposed encodings shows that the
reachability relation is very effective and leads to comparable performance to
a state-of-the-art S5 solver based on SAT, while entailment relations are
possibly too expensive to reason about and may result in overhead. This paper
is under consideration for acceptance in TPLP.
Related papers
- Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning [1.3003982724617653]
Large Language Models (LLMs) have revolutionized natural language processing, yet they struggle with inconsistent reasoning.
This research introduces Proof of Thought, a framework that enhances the reliability and transparency of LLM outputs.
Key contributions include a robust type system with sort management for enhanced logical integrity, explicit representation of rules for clear distinction between factual and inferential knowledge.
arXiv Detail & Related papers (2024-09-25T18:35:45Z) - The Foundations of Tokenization: Statistical and Computational Concerns [51.370165245628975]
Tokenization is a critical step in the NLP pipeline.
Despite its recognized importance as a standard representation method in NLP, the theoretical underpinnings of tokenization are not yet fully understood.
The present paper contributes to addressing this theoretical gap by proposing a unified formal framework for representing and analyzing tokenizer models.
arXiv Detail & Related papers (2024-07-16T11:12:28Z) - When Do Program-of-Thoughts Work for Reasoning? [51.2699797837818]
We propose complexity-impacted reasoning score (CIRS) to measure correlation between code and reasoning abilities.
Specifically, we use the abstract syntax tree to encode the structural information and calculate logical complexity.
Code will be integrated into the EasyInstruct framework at https://github.com/zjunlp/EasyInstruct.
arXiv Detail & Related papers (2023-08-29T17:22:39Z) - ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
We characterize several different forms of compositional generalization that are desirable in program synthesis.
We propose ExeDec, a novel decomposition-based strategy that predicts execution subgoals to solve problems step-by-step informed by program execution at each step.
arXiv Detail & Related papers (2023-07-26T01:07:52Z) - From Robustness to Explainability and Back Again [0.685316573653194]
The paper addresses the limitation of scalability of formal explainability, and proposes novel algorithms for computing formal explanations.
The proposed algorithm computes explanations by answering instead a number of robustness queries, and such that the number of such queries is at most linear on the number of features.
The experiments validate the practical efficiency of the proposed approach.
arXiv Detail & Related papers (2023-06-05T17:21:05Z) - Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving [0.3441021278275805]
Probabilistic programming combines general computer programming, statistical inference, and formal semantics.
ProbURel is based on Hehner's predicative probabilistic programming, but there are several obstacles to the broader adoption of his work.
Our contributions include the formalisation of relations using Unifying Theories of Programming (UTP) and probabilities outside the brackets.
We demonstrate our work with six examples, including problems in robot localisation, classification in machine learning, and the termination of probabilistic loops.
arXiv Detail & Related papers (2023-03-16T23:36:57Z) - Semantic-aware Modular Capsule Routing for Visual Question Answering [55.03883681191765]
We propose a Semantic-aware modUlar caPsulE framework, termed as SUPER, to better capture the instance-specific vision-semantic characteristics.
We comparatively justify the effectiveness and generalization ability of our proposed SUPER scheme over five benchmark datasets.
arXiv Detail & Related papers (2022-07-21T10:48:37Z) - Rationale-Augmented Ensembles in Language Models [53.45015291520658]
We reconsider rationale-augmented prompting for few-shot in-context learning.
We identify rationale sampling in the output space as the key component to robustly improve performance.
We demonstrate that rationale-augmented ensembles achieve more accurate and interpretable results than existing prompting approaches.
arXiv Detail & Related papers (2022-07-02T06:20:57Z) - 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) - Adaptive n-ary Activation Functions for Probabilistic Boolean Logic [2.294014185517203]
We show that we can learn arbitrary logic in a single layer using an activation function of matching or greater arity.
We represent belief tables using a basis that directly associates the number of nonzero parameters to the effective arity of the belief function.
This opens optimization approaches to reduce logical complexity by inducing parameter sparsity.
arXiv Detail & Related papers (2022-03-16T22:47:53Z) - String Theories involving Regular Membership Predicates: From Practice
to Theory and Back [12.98284167710378]
An algorithm for the satisfiability problem for systems of string constraints requires a thorough understanding of the structure of constraints present in the targeted cases.
In this paper, we investigate benchmarks presented in the literature containing regular expression membership predicates, extract different first order logic theories, and prove their decidability undecidability.
Notably, the most common theories in real-world benchmarks are PSPACE-complete and directly lead to the implementation of a more efficient algorithm to solving string constraints.
arXiv Detail & Related papers (2021-05-15T13:13:50Z)
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.