Automata for dynamic answer set solving: Preliminary report

• URL: http://arxiv.org/abs/2109.01782v1
• Date: Sat, 4 Sep 2021 03:58:12 GMT
• Title: Automata for dynamic answer set solving: Preliminary report
• Authors: Pedro Cabalar (1), Mart\'in Di\'eguez (2), Susana Hahn (3), Torsten Schaub (3) ((1) University of Corunna, Spain, (2) Universit\'e d'Angers, France, (3) University of Potsdam, Germany)
• Abstract summary: We explore different ways of implementing temporal constraints expressed in an extension of Answer Set Programming (ASP) with language constructs from dynamic logic. The idea is to transform a dynamic constraint into an automaton expressed in terms of a logic program that enforces the satisfaction of the original constraint.
• Score: 0.0
• License: http://creativecommons.org/publicdomain/zero/1.0/
• Abstract: We explore different ways of implementing temporal constraints expressed in an extension of Answer Set Programming (ASP) with language constructs from dynamic logic. Foremost, we investigate how automata can be used for enforcing such constraints. The idea is to transform a dynamic constraint into an automaton expressed in terms of a logic program that enforces the satisfaction of the original constraint. What makes this approach attractive is its independence of time stamps and the potential to detect unsatisfiability. On the one hand, we elaborate upon a transformation of dynamic formulas into alternating automata that relies on meta-programming in ASP. This is the first application of reification applied to theory expressions in gringo. On the other hand, we propose two transformations of dynamic formulas into monadic second-order formulas. These can then be used by off-the-shelf tools to construct the corresponding automata. We contrast both approaches empirically with the one of the temporal ASP solver telingo that directly maps dynamic constraints to logic programs. Since this preliminary study is restricted to dynamic formulas in integrity constraints, its implementations and (empirical) results readily apply to conventional linear dynamic logic, too.

Related papers

• COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
  Iterative refinement has emerged as an effective paradigm for enhancing the capabilities of large language models (LLMs) on complex tasks. We propose Context-Wise Order-Agnostic Language Modeling (COrAL) to overcome these challenges. Our approach models multiple token dependencies within manageable context windows, enabling the model to perform iterative refinement internally.
  arXiv  Detail & Related papers  (2024-10-12T23:56:19Z)
• H-STAR: LLM-driven Hybrid SQL-Text Adaptive Reasoning on Tables [56.73919743039263]
  This paper introduces a novel algorithm that integrates both symbolic and semantic (textual) approaches in a two-stage process to address limitations. Our experiments demonstrate that H-STAR significantly outperforms state-of-the-art methods across three question-answering (QA) and fact-verification datasets.
  arXiv  Detail & Related papers  (2024-06-29T21:24:19Z)
• Shape Arithmetic Expressions: Advancing Scientific Discovery Beyond Closed-Form Equations [56.78271181959529]
  Generalized Additive Models (GAMs) can capture non-linear relationships between variables and targets, but they cannot capture intricate feature interactions. We propose Shape Expressions Arithmetic ( SHAREs) that fuses GAM's flexible shape functions with the complex feature interactions found in mathematical expressions. We also design a set of rules for constructing SHAREs that guarantee transparency of the found expressions beyond the standard constraints.
  arXiv  Detail & Related papers  (2024-04-15T13:44:01Z)
• Discret2Di -- Deep Learning based Discretization for Model-based Diagnosis [48.252498836623154]
  consistency-based diagnosis is an established approach to diagnose technical applications, but suffers from significant modeling efforts. This paper presents the methodology Discret2Di for automated learning of logical expressions for consistency-based diagnosis. The solution presented combines machine learning from both the time series and the symbolic domain to automate the learning of logical rules for consistency-based diagnosis.
  arXiv  Detail & Related papers  (2023-11-06T09:17:57Z)
• Large Language Models as General Pattern Machines [64.75501424160748]
  We show that pre-trained large language models (LLMs) are capable of autoregressively completing complex token sequences. Surprisingly, pattern completion proficiency can be partially retained even when the sequences are expressed using tokens randomly sampled from the vocabulary. In this work, we investigate how these zero-shot capabilities may be applied to problems in robotics.
  arXiv  Detail & Related papers  (2023-07-10T17:32:13Z)
• Metric Temporal Equilibrium Logic over Timed Traces [1.2657785774485026]
  We develop a metric extension of linear-time temporal equilibrium logic, in which temporal operators are constrained by intervals over natural numbers. The resulting Metric Equilibrium Logic provides the foundation of an ASP-based approach for specifying qualitative and quantitative dynamic constraints.
  arXiv  Detail & Related papers  (2023-04-28T11:39:49Z)
• Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming [2.3204178451683264]
  We present a variation of the top-down evaluation strategy, termed Dynamic Consistency checking. This makes it possible to determine when a literal is not compatible with the denials associated to the global constraints in the program. We have experimentally observed speedups of up to 90x w.r.t. the standard versions of s(CASP)
  arXiv  Detail & Related papers  (2021-10-22T20:38:48Z)
• Automata Techniques for Temporal Answer Set Programming [0.0]
  Temporal and dynamic extensions of Answer Set Programming (ASP) have played an important role in addressing dynamic problems. I intend to exploit the relationship between automata theory and dynamic logic to add automata-based techniques to the ASP solver CLINGO.
  arXiv  Detail & Related papers  (2021-09-17T01:43:31Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Temporal Answer Set Programming [3.263632801414296]
  We present an overview on Temporal Logic Programming under the perspective of its application for Knowledge Representation and declarative problem solving. We focus on recent results of the non-monotonic formalism called Temporal Equilibrium Logic (TEL) that is defined for the full syntax. In a second part, we focus on practical aspects, defining a syntactic fragment called temporal logic programs closer to ASP, and explain how this has been exploited in the construction of the solver TELINGO.
  arXiv  Detail & Related papers  (2020-09-14T16:13:36Z)
• Implementing Dynamic Answer Set Programming [0.0]
  We develop a translation of dynamic formulas into temporal logic programs. The reduction of dynamic formulas to temporal logic programs allows us to extend ASP with both approaches in a uniform way.
  arXiv  Detail & Related papers  (2020-02-17T12:34:14Z)

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.