LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:exists-forall_class_definition [2009/05/14 13:09]
vkuncak
sav08:exists-forall_class_definition [2010/05/03 11:17]
vkuncak
Line 1: Line 1:
-====== Exists-Forall Class Definition ======+====== Exists-Forall Class (EPR, BSR) Definition ======
  
 Also called [[wp>​Paul Bernays|Berneys]]-[[wp>​Schoenfinkel]] class and Effectively Propositional Logic (EPR). Also called [[wp>​Paul Bernays|Berneys]]-[[wp>​Schoenfinkel]] class and Effectively Propositional Logic (EPR).
Line 25: Line 25:
 List contains no duplicates: List contains no duplicates:
 \[ \[
-   ​\forall x,y. ListNode(x) \land ListNode(y) \land data(x) ​data(y) \rightarrow x=y+   ​\forall x,y,z. ListNode(x) \land ListNode(y) \land data(x,z\land data(y,z) \rightarrow x=y
 \] \]