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
- Think Beyond Size: Adaptive Prompting for More Effective Reasoning [0.0]
We introduce Adaptive Prompting, a dynamic and iterative framework designed to enhance reasoning by incorporating real-time adjustments to prompt structures and validation mechanisms.
Results demonstrate that Adaptive Prompting significantly improves performance on diverse reasoning benchmarks, including arithmetic reasoning (GSM8K, MultiArithm), logical reasoning and commonsense tasks.
Our approach enables smaller models to achieve competitive performance with larger counterparts, such as GPT-4, while maintaining computational efficiency.
arXiv Detail & Related papers (2024-10-10T17:14:36Z) - 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) - Large Language Models as an Indirect Reasoner: Contrapositive and Contradiction for Automated Reasoning [74.90592233107712]
We propose a Direct-Indirect Reasoning (DIR) method, which considers Direct Reasoning (DR) and Indirect Reasoning (IR) as multiple parallel reasoning paths that are merged to derive the final answer.
Our DIR method is simple yet effective and can be straightforwardly integrated with existing variants of CoT methods.
arXiv Detail & Related papers (2024-02-06T03:41:12Z) - 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 [3.7950144463212134]
This paper addresses the poor scalability of formal explainability and proposes novel efficient algorithms for computing formal explanations.
The proposed algorithm computes explanations by answering instead a number of queries, and such robustness that the number of such queries is at most linear on the number of features.
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.