separate tree structure from modal information

[shaolintl]

We remove modal information from the tree and put it in a separate data structure. Data in the data structure can be mapped to tree nodes. But we can also replace them by variables and then allow the search to decide which boxes and diamonds on which tree node.

This should also lead, hopefully, to the case we omit the tree completely and give only the essential information of the relationship between boxes and diamonds.

[shaolintl]

we need also to separate by adding another list the information for the initial rule

[shaolintl]

Marco happily volunteered. Thanks Marco!

[emmevolpe]

One issue related to this is that we might have more boxes for a given diamond.

@shaolintl : I see two solutions for it and I would like to hear your opinion before implementing.
In both cases, the proof evidence would be specified by:

• a tree (specifying the formulas on which to decide);
• a list (associating diamonds to corresponding boxes);
• a list (associating literals to complementary literals).

1. We keep the tree structure as it is now, i.e., containing nodes which are pairs. This means possibly duplicating the information in the tree and in the lists and checking both when, e.g., a diamond is instantiated. Of course both the tree and the lists can contain variables instead of concrete indexes.
2. We remove the second element in the tree nodes and let the lists contain triples of the form, e.g., (position_in_the_tree, index_of_diamond, index_of_box). This requires however, during the checking process, keeping track in the proof certificate of the current position in the tree (we don't do it at the moment).

[shaolintl]

@emmevolpe Can you clarify on the two options?

1. What happens if we want to supply only box-diamond information? Do we put a variable for the entire tree? But what about the optional information in the nodes which will be reset?
2. This sounds better from the reason above. Why isnt the position of a node sufficient? Why do we need the current position?

[emmevolpe]

1. In that case I would say: the tree is a variable and the "position_in_the_tree" field is a variable too for all the elements in the list.
2. The "position_in_the_tree" field should refer to the position in the original derivation tree, which is something different from the indexes denoting formulas. We need the current position in order to understand which entry in the list we are looking for.

[emmevolpe]

All in all, I think that 1 is easier to implement (FPC closer to what we have now) and that it makes it also easier to write down examples. It brings in some redundancy though, which is not nice. And at each diamond/initial one should check in two places: might this affect efficiency?

[shaolintl]

Not if we check that the two places have the same value at the same time. This will be the moment we try to replace the variables with terms and there will be only one option.

[emmevolpe]

I would go for 2. It seems a bit more painful but cleaner to me. I don't like data structures with redundancies.

[shaolintl]

After a long brainstorming with Marco, we reached the conclusion of combing the two fpcs into one and change our certificate into two certificates. In this way, one can leave the other as a variable and get current behavior. One can also put variables in both and get even sparser certificates.

[shaolintl]

A new suggestion:
We will have a generic format:

1. decide tree
2. box-dia indices
3. initial indices

The implementation of the indices will determine the amount of preciseness. I.e. if the dia index is a formula location index, then it will not identify precisely in the proof tree. If the dia index is a proof tree index (or formula index and a counter), then it identifies precisely.

Two possible uses:

1. Full decide tree and indices within the proof tree (deterministic)
2. var for decide tree and indices for formula location (non-deterministic)

We can also have other options in between.

We will create one FPC which will abstract over the get_dia and get_initial relations. These relations are supposed to be able to return the right eigenvariable for the dia and the index of the complementary literal

Their input will be the decide tree, the relative map (dia or init) and the index chosen

@emmevolpe Objections?

[shaolintl]

@emmevolpe Trying to understand the (non-documented) simpfit certificate format:

kind closure, boxinfo, use type.
type closure index -> index -> closure.
type boxinfo index -> index -> boxinfo.
type use index -> use.
type simpfit int -> list index -> list closure -> list boxinfo -> list (pair index atm) -> list use -> cert.

We need list closure and list boxinfo, what are the other three lists?