String Theories involving Regular Membership Predicates: From Practice to Theory and Back

• URL: http://arxiv.org/abs/2105.07220v1
• Date: Sat, 15 May 2021 13:13:50 GMT
• Title: String Theories involving Regular Membership Predicates: From Practice to Theory and Back
• Authors: Murphy Berzish, Joel D. Day, Vijay Ganesh, Mitja Kulczynski, Florin Manea, Federico Mora, Dirk Nowotka
• Abstract summary: 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.
• Score: 12.98284167710378
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Widespread use of string solvers in formal analysis of string-heavy programs has led to a growing demand for more efficient and reliable techniques which can be applied in this context, especially for real-world cases. Designing an algorithm for the (generally undecidable) 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, resp. 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.

Related papers

• A novel framework for systematic propositional formula simplification based on existential graphs [1.104960878651584]
  This paper presents a novel simplification calculus for propositional logic derived from Peirce's existential graphs' rules of inference and implication graphs. Our rules can be applied to propositional logic formulae in nested form, are equivalence-preserving, guarantee a monotonically decreasing number of variables, clauses and literals, and maximise the preservation of structural problem information.
  arXiv  Detail & Related papers  (2024-05-27T11:42:46Z)
• Multitask Kernel-based Learning with Logic Constraints [13.70920563542248]
  This paper presents a framework to integrate prior knowledge in the form of logic constraints among a set of task functions into kernel machines. We consider a multi-task learning scheme, where multiple unary predicates on the feature space are to be learned by kernel machines. A general approach is presented to convert the logic clauses into a continuous implementation, that processes the outputs computed by the kernel-based predicates.
  arXiv  Detail & Related papers  (2024-02-16T12:11:34Z)
• Optimised Storage for Datalog Reasoning [8.305527776204178]
  Materialisation facilitates Datalog reasoning by precomputing all consequences of the facts and the rules so that queries can be directly answered over the materialised facts. storing all materialised facts may be infeasible in practice, especially when the rules are complex and the given set of facts is large. We present a general framework that allows for the integration of such optimised storage schemes with standard materialisation algorithms.
  arXiv  Detail & Related papers  (2023-12-18T15:46:10Z)
• An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
  This approach allows for the computer-assisted analysis of abstract dialectical frameworks. Exemplary applications include the formal analysis and verification of meta-theoretical properties.
  arXiv  Detail & Related papers  (2023-12-08T09:32:26Z)
• Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
  We propose a structure-modeled textual encoding framework for inductive logical reasoning over KGs. It encodes linearized query structures and entities using pre-trained language models to find answers. We conduct experiments on two inductive logical reasoning datasets and three transductive datasets.
  arXiv  Detail & Related papers  (2023-05-23T01:25:29Z)
• Synergies between Disentanglement and Sparsity: Generalization and Identifiability in Multi-Task Learning [79.83792914684985]
  We prove a new identifiability result that provides conditions under which maximally sparse base-predictors yield disentangled representations. Motivated by this theoretical result, we propose a practical approach to learn disentangled representations based on a sparsity-promoting bi-level optimization problem.
  arXiv  Detail & Related papers  (2022-11-26T21:02:09Z)
• 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)
• Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments [12.952483242045366]
  We investigate practical algorithms for inconsistency-tolerant query answering over prioritized knowledge bases. We consider three well-known semantics (AR, IAR and brave) based upon two notions of optimal repairs (Pareto and completion)
  arXiv  Detail & Related papers  (2022-02-16T10:44:39Z)
• Modal Logic S5 Satisfiability in Answer Set Programming [8.89493507314525]
  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.
  arXiv  Detail & Related papers  (2021-08-09T17:35:31Z)
• Fractal Structure and Generalization Properties of Stochastic Optimization Algorithms [71.62575565990502]
  We prove that the generalization error of an optimization algorithm can be bounded on the complexity' of the fractal structure that underlies its generalization measure. We further specialize our results to specific problems (e.g., linear/logistic regression, one hidden/layered neural networks) and algorithms.
  arXiv  Detail & Related papers  (2021-06-09T08:05:36Z)
• Learning Implicitly with Noisy Data in Linear Arithmetic [94.66549436482306]
  We extend implicit learning in PAC-Semantics to handle intervals and threshold uncertainty in the language of linear arithmetic. We show that our implicit approach to learning optimal linear programming objective constraints significantly outperforms an explicit approach in practice.
  arXiv  Detail & Related papers  (2020-10-23T19:08:46Z)

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.