search

salmans / Razor

5 stars 0 forks source link

Provenance for Constants #4

Closed salmans closed 10 years ago

salmans commented 10 years ago

Construct provenance information for constants. @vpatara

salmans commented 10 years ago

This implementation adds a new provenance information for every occurrence of a constants. For example given a theory: 1: Truth => P(a()) 2: Truth => Q(a())

it creates two provenances for a(), one with tag 1 and sequent number 1 and another with tag 2 and sequent number 2.

tuna-salad commented 10 years ago

The provenance doesn't explicitly say which element is equal to a() or b(), though the model says that. I think it is more regular to instead add, say, a(e#1) because we consider a() = e#1 as a relational fact a(e#1) anyway. Now I rely on all the information in the provenance.

Moreover, concerning #8, using (Fct (F constName [element])) to replace Den in provenance can fix that problem in #8 without having to deal with Den later.

salmans commented 10 years ago

Since a() is a nullary function, a(e#1) is syntactically invalid. Instead, we may construct provenance for "a() = e#1". The next commit will implement this idea.

tuna-salad commented 10 years ago

Can you describe more what it means to be syntactically invalid? Why do we have to treat nullary functions differently from other functions when we convert functions to relations?