Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

Decision procedures can be either theory specific, e.g., Presburger arithmetic, or theory-generic, applying to an infinite number of user-definable theories. Variant satisfiability is a theory-generic procedure for quantifier-free satisfiability in the initial algebra of an order-sorted equational theory (Σ, E ∪ B)$ under two conditions: (i) E ∪ B has the finite variant property and B has a finitary unification algorithm; and (ii) (Σ, E ∪ B) protects a constructor subtheory (Ω, E(Ω) ∪ B(Ω))$ that is OS-compact. These conditions apply to many user-definable theories, but have a main limitation: they apply well to data structures, but often do not hold for user-definable predicates on such data structures. We present a theory-generic satisfiability decision procedure, and a prototype implementation, extending variant-based satisfiability to initial algebras with user-definable predicates under fairly general conditions.

On the installation and use

The decision procedure has been implemented entirely in Maude using its reflection capabilities. The latest version of the tool works on Maude 2.6.

To load the tool one just needs to load the Maude code of the tool. If maude is your Maude executable, the call to the decision procedure is in file nu-itp.maude, and all files are in the same directory, you can load the tool as follows:

$ maude nu-itp.maude
             \||||||||||||||||||/
           --- Welcome to Maude ---
             /||||||||||||||||||\
        Maude 2.6 built: Dec 10 2010 11:12:39
        Copyright 1997-2010 SRI International
           Sat May 7 21:19:03 2011
Maude>

The decision procedure offers the following command:

red initTheory(<whole-theory-module>, <preds-theory-module>, <os-compact-theory-module>, <conjectures-and-patterns-module>) .

For instance, consider the main example of the paper. The union of modules ACU-NAT-FUN and NAT-SET specifies the equational theory NatSet. NAT-SET itself specifies the OS-compact constructor decomposition of the theory.


fmod ACU-NAT is
  sort Natural .

  op 0   : -> Natural [ctor] .
  op 1   : -> Natural [ctor] .
  op _+_ : Natural Natural -> Natural [ctor assoc comm id: 0] .
endfm

fmod ACU-NAT-FUN is
  pr ACU-NAT .

  op max : Natural Natural -> Natural [comm] .
  op min : Natural Natural -> Natural [comm] .
  op _-_ : Natural Natural -> Natural .  *** monus

  vars N M : Natural .

  eq max(N,N + M) = N + M [variant] .
  eq min(N,N + M) = N [variant] .

  eq N - (N + M) = 0 [variant].
  eq (N + M) - N = M [variant] .
endfm

fmod ACU-NAT-SET is
  pr ACU-NAT .

  sort NaturalSet .

  subsort Natural < NaturalSet .

  op mt : -> NaturalSet [ctor] .
  op _,_ : NaturalSet NaturalSet -> NaturalSet [ctor assoc comm] .

  vars NS NS' : NaturalSet .

  *** identity of set union
  eq NS , mt = NS [variant] .
  *** idempotency of set union
  eq NS , NS = NS [variant] .
  *** idempotency of set union
  eq NS , NS , NS' = NS , NS' [variant] .
 endfm

The extension NatSetPreds of the theory NatSet is specified by the NAT-SET-PREDS module.

  
fmod ACU-NAT-SET-PREDS is
  pr ACU-NAT-SET .

  sort Pred .

  op tt : -> Pred [ctor] .
  *** set containment
  op _=C_ : NaturalSet NaturalSet -> Pred [ctor] .
  *** strict order
  op _>_ : Natural Natural -> Pred [ctor] .   
  *** sort predicates
  op natural : NaturalSet -> Pred [ctor] .
  op even : NaturalSet -> Pred [ctor] .
  op odd : NaturalSet -> Pred [ctor] .

  vars N M : Natural .
  vars NS NS' : NaturalSet .

  eq mt =C NS = tt [variant] .
  eq NS =C NS = tt [variant] .
  eq NS =C NS , NS' = tt [variant] .

  eq N + M + 1 > N = tt [variant] .

  eq natural(N) = tt [variant] .

  eq even(N + N) = tt [variant] .
  
  eq odd(N + N + 1) = tt [variant] .
endfm

A QF formula we want to test for variant satisfiability is specified as a non-executable equations labeled with the conjecture keyword. The negative patterns of each user-defined predicate outside the OS-compact subtheory are also specified as non-executable equations labeled with the nPattern keyword. Suppose we want to prove the inductive validity of the following formulae:

N - M = 0 ⇔ M > N = tt ∨ N = M, and
natural(NS) = tt ⇒ even(NS) = tt ∨ odd(NS) = tt.

This is equivalent to proving that each conjunction in the DNF of each negated formula is unsatisfiable. Therefore, our input conjectures are:

(N - M = 0 ∧ M > N ≠ tt ∧ N ≠ M) ∨ (N - M ≠ 0 ∧ M > N = tt) ∨ (N - M ≠ 0 ∧ N = M) for the first formula, and
natural(NS) = tt ∧ even(NS) ≠ tt ∧ odd(NS) ≠ tt for the second formula.

The three conjunctions of the first formula correspond to the equations prop1a, prop1b and prop1c in module NAT-SET-PRED-CONJECTURES-PATTERNS, and the second formula corresponds to the equation prop2. We also specify in module NAT-SET-PRED-CONJECTURES-PATTERNS the negative patterns.


mod ACU-NAT-SET-PREDS-CONJECTURES-PATTERNS is
  pr ATOM-MAGMA-SET .
  pr PATTERN .
  pr ACU-NAT-SET-PREDS .
  pr ACU-NAT-FUN .

*** patterns
  op neg-subseteq : NaturalSet NaturalSet -> Pattern .
  op neg-gr      : Natural Natural -> Pattern .
  op neg-even    : NaturalSet -> Pattern .
  op neg-odd     : NaturalSet -> Pattern .
  op neg-natural : NaturalSet -> Pattern .

*** formulae
  op prop1a : Natural Natural -> AtomMagma .
  op prop1b : Natural Natural -> AtomMagma .
  op prop1c : Natural Natural -> AtomMagma .
  op prop2  : NaturalSet -> AtomMagma .

  vars N M K : Natural .
  var NS : NaturalSet .
  
  eq prop1a(N,M) = (N - M = 0) , (M > N /= tt) 
       , (N /= M) [nonexec label conjecture] .
  eq prop1b(N,M) = (N - M /= 0) 
       , (M > N = tt) [nonexec label conjecture] .
  eq prop1c(N,M) = (N - M /= 0) 
       , (N = M) [nonexec label conjecture] .

  eq prop2(NS) = (natural(NS) = tt) , (even(NS) /= tt) 
       , (odd(NS) /= tt) [nonexec label conjecture] .

  eq neg-subseteq(NS,MS) = NS =C MS
       | ((NS, MS) /= MS) [nonexec label nPattern] .
  eq neg-gr(N,M) = N > N + M 
       | (empty).AtomMagma [nonexec label nPattern] .
  eq neg-even(mt) = even(mt)
       | (empty).AtomMagma [nonexec label nPattern] .
  eq neg-even(N) = even(N + N + 1) 
       | (empty).AtomMagma [nonexec label nPattern] .
  eq neg-even((N , NS)) = even((N, NS)) 
       | ((N /= NS) , (NS /= mt)) [nonexec label nPattern] . 
  eq neg-odd(mt) = odd(mt)
       | (empty).AtomMagma [nonexec label nPattern] .
  eq neg-odd(N) = odd(N + N) 
       | (empty).AtomMagma [nonexec label nPattern] .
  eq neg-odd((N , NS)) = odd((N, NS)) 
       | ((N /= NS) , (NS /= mt)) [nonexec label nPattern] .
  eq neg-natural(mt) = natural(mt)
       | (empty).AtomMagma [nonexec label nPattern] .
  eq neg-natural((N , NS)) = natural((N, NS)) 
       | ((N /= NS) , (NS /= mt)) [nonexec label nPattern] .
endm

In the execution, our main function uses four arguments:

the whole theory (Σ,E ∪ U),
the subtheory that contains the predicates,
the constructor subtheory (Ω,E(Ω) ∪ B(Ω)) which is OS-compact, and
the patterns and the conjectures.


fmod ACU-NAT-SET-PREDS-THEORY is
  pr ACU-NAT-SET-PREDS .
  pr ACU-NAT-FUN .
endfm

fmod ACU-NAT-SET-PREDS-INTERFACE is
  pr ACU-NAT-SET-PREDS-THEORY .
  pr NU-ITP-INTERFACE .
endfm

red in ACU-NAT-SET-PREDS-INTERFACE : 
  initTheory(upModule('NAT-SET-PREDS-THEORY,true)
    , upModule('ACU-NAT-SET-PREDS,true)
    , upModule('ACU-NAT-SET,true)
    , upModule('ACU-NAT-SET-PREDS-CONJECTURES-PATTERNS
        ,false)) .

If the result is {false} then the formula is unsatisfiable and if it is {true} then the formula is satisfiable.

Download

You need:

Documentation

Variant Satisfiability in Initial Algebras with Predicates (long version). Raúl Gutiérrez and José Meseguer. Technical Report, Department of Computer Science in the University of Illinois at Urbana-Champaign. Urbana, June 2017.

11/15/2017