Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Equational Theorem Proving for Clauses over Strings

Dohan Kim

TL;DR

This work addresses the challenge of performing equational theorem proving for clauses over strings under a monotonicity assumption. It introduces a novel refutationally complete superposition calculus, with a lifting mechanism to $g$-terms/$g$-clauses and contraction-based redundancy management, enabling saturation-based decision procedures for word problems when the conditional theory $R$ is finitely saturable. A key contribution is the model-based completeness proof and a framework that translates clauses over strings into a first-order representation to leverage established techniques, while preserving reversibility via a lifting schema. The results lay the groundwork for robust string-constraint reasoning in verification and language-theoretic contexts and open avenues for incorporating built-in equational theories in future work.

Abstract

Although reasoning about equations over strings has been extensively studied for several decades, little research has been done for equational reasoning on general clauses over strings. This paper introduces a new superposition calculus with strings and present an equational theorem proving framework for clauses over strings. It provides a saturation procedure for clauses over strings and show that the proposed superposition calculus with contraction rules is refutationally complete. This paper also presents a new decision procedure for word problems over strings w.r.t. a set of conditional equations R over strings if R can be finitely saturated under the proposed inference system.

Equational Theorem Proving for Clauses over Strings

TL;DR

This work addresses the challenge of performing equational theorem proving for clauses over strings under a monotonicity assumption. It introduces a novel refutationally complete superposition calculus, with a lifting mechanism to -terms/-clauses and contraction-based redundancy management, enabling saturation-based decision procedures for word problems when the conditional theory is finitely saturable. A key contribution is the model-based completeness proof and a framework that translates clauses over strings into a first-order representation to leverage established techniques, while preserving reversibility via a lifting schema. The results lay the groundwork for robust string-constraint reasoning in verification and language-theoretic contexts and open avenues for incorporating built-in equational theories in future work.

Abstract

Although reasoning about equations over strings has been extensively studied for several decades, little research has been done for equational reasoning on general clauses over strings. This paper introduces a new superposition calculus with strings and present an equational theorem proving framework for clauses over strings. It provides a saturation procedure for clauses over strings and show that the proposed superposition calculus with contraction rules is refutationally complete. This paper also presents a new decision procedure for word problems over strings w.r.t. a set of conditional equations R over strings if R can be finitely saturated under the proposed inference system.
Paper Structure (10 sections, 13 theorems)

This paper contains 10 sections, 13 theorems.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Superposition with Strings
  4. Inference Rules
  5. Lifting Properties
  6. Redundancy and Contraction Techniques
  7. Refutational Completeness
  8. Conditional Completion
  9. Related Work
  10. Conclusion

Key Result

Lemma 1

Let $C:=s_1\approx t_1\vee\cdots\vee s_m \approx t_m \vee u_1\not\approx v_1 \vee\cdots \vee u_n \not\approx v_n$ be a clause over $\Sigma^*$ and $P$ be the set of all clauses that follow from $C$ using the monotonicity property. Let $Q$ be the set of all ground instances of the clause $s_1(x_1)\app

Theorems & Definitions (40)

  • Example 1
  • Example 2
  • Lemma 1
  • proof
  • Definition 2
  • Example 3
  • Example 4
  • Definition 3
  • Definition 4
  • Lemma 5
  • ...and 30 more