back to root

back to Matryoshka

Defintion of the TRS with booleans

• Alexander Bentkamp

  2020-04-07 16:13:17 (GMT)

  Hi, I could use some opinions on my definition of the TRS in the beginning of the section "Ground refutational completeness" in the draft (now papers/2021-fboolsup).

  It looks a bit too complicated for what it's supposed to do. The idea is the following: As in first-order superposition, the TRS is constructed by going through all clauses in N in increasing order. Because of how the clause order works, the iteration through all clauses can be partitioned in stages, one for each term $s$, where the stage for $s$ consists of all clauses whose maximal term is $s$. As in first-order, under certain conditions, we add a rewrite rule $s \rightarrow t$ if the maximal literal is $s \approx t$. But in addition, before and after each stage I want to add a few additional rewrite rules to take care of the boolean connectives.

  Right now, I am using a trick to achieve this. Instead of iterating over the clauses in N, I iterate over all clauses. I use the first- and the second smallest clause $s \approx \top$ and $s \approx \bot$ of each stage to detect the beginning of a stage and the clause $s \not\approx \top$, which happens to be large enough, to detect the "end" of a stage.

• Petar Vukmirovic

  2020-04-07 16:29:53 (GMT)

  what additional RW rules are you adding

• Alexander Bentkamp

  2020-04-07 16:35:31 (GMT)

  Rewrites like $\forall x. t[x] \rightarrow \top$ if $t[u]$ normalizes to $\top$ for all $u$.

• Alexander Bentkamp

  2020-04-07 16:37:49 (GMT)

  and also a rewrite $s \rightarrow \bot$ if $s$ is not reducible

• Alexander Bentkamp

  2020-04-07 16:38:21 (GMT)

  Essentially, I have to make sure that $\top$ and $\bot$ are the only normal forms of type bool.

• Petar Vukmirovic

  2020-04-07 16:46:17 (GMT)

  yeah, sorry this might be out my realm of skills :frown:

• Jasmin Blanchette

  2020-04-07 17:15:47 (GMT)

  Me too, but I'm guessing Visa will be happy that there are only two normal forms. ;)

• Sophie

  2020-04-07 18:55:21 (GMT)

  The only thing that I really wonder about is whether adding these extra rewrite rules on the fly is really necessary. Can't you add these rules afterward by iterating on all unit (dis-)equalities between Booleans where the right-hand side is constant (and where s is not reducible in R_N)? In the general case, it would be problematic to do this separately due to the bad interactions with other rules, but since all the rules you add in B, C and D are terminal, it could possibly work, and it would (maybe) make the presentation a bit cleaner and closer to what is usual.

• Sophie

  2020-04-07 19:1:28 (GMT)

  The second phase could then maybe even be restricted to unit Boolean clauses of the form $t\approx\top$ (and the other two forms) but where $t$ appears in the right-hand side of a rule in R_N.

• Alexander Bentkamp

  2020-04-07 19:2:29 (GMT)

  That might be a good idea. The issue with it is that I some of the conditions are referring to the TRS $R_C$ that has been constructed so far. And at the moment I am relying on the fact that these $R_C$ contain the rules for the boolean connectives already.

• Sophie

  2020-04-07 19:7:3 (GMT)

  ... then it is not a good idea ^^' ... except if you can prove that only the ones with a $t$ are useful, but I have no idea if that is true or if it wouldn't make the proof messier.

• Sophie

  2020-04-07 19:8:2 (GMT)

  You can always start with a proof where they are mixed to see if you can go through and later on come back to this idea and see if the proof can be transformed.

• Alexander Bentkamp

  2020-04-07 19:12:7 (GMT)

  I still think that it can be done essentially as you suggested. Only the conditions referring to $R_C$ have to refer to some modified version $R_C^*$ of $R_C$ that contains the rules for boolean connectives.

• Alexander Bentkamp

  2020-04-07 19:13:44 (GMT)

  But yes, maybe I am trying too hard to get the definitions right from the start...

• Ahmed B

  2020-04-08 16:28:4 (GMT)

  Just look through the stub and (some) of the comments above and I am very impressed!

  It seems to me that what you are attempting to achieve with these extra rules in B, C and D is to normalise the interpreted boolean appearing in clauses in N?

  Could you not add the rewrite rules for these booleans to the TRS first? I.e. define the set of terms with interpreted boolean heads that appear in any clause in N at any position. Then, build a rewrite system based on these terms, call it $R_B$. Then define $R_C$ for $C \in N$ as $R_B \cup \cup_{D \prec C} \Delta_D$ . This is very similar to what we do for the cominator axioms in our proof. In a similar manner we need the combinator equations to be true at various points in the induction.

• Ahmed B

  2020-04-08 16:30:27 (GMT)

  image.png

  

  The first step in the proof doesn't appear to hold. The rewrite could be beneath a quantifier in which case there would be no sup inference at that position?

• Alexander Bentkamp

  2020-04-08 16:33:49 (GMT)

  Could you not add the rewrite rules for these booleans to the TRS first?

  For the connectives, yes. But for the quantifiers I need to wait because I need to know whether a the formula in question holds for all terms or not.

• Alexander Bentkamp

  2020-04-08 16:41:51 (GMT)

  I just pushed a new definition in the style Sophie proposed. This makes it much shorter and maybe a tiny bit more intuitive.

• Alexander Bentkamp

  2020-04-08 16:42:42 (GMT)

  The first step in the proof doesn't appear to hold. The rewrite could be beneath a quantifier in which case there would be no sup inference at that position?

  It's a really sketchy proof sketch :D

  But I think I can make it work. If the rewrite is below a quantifier, that means there is a quantifier, which must be reducible to true or false. Then I can use the second case instead.