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 [2008/04/03 13:42]
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).
  
 Notation according to [[Classical Decision Problem]] classification:​ $[\exists^* \forall^*,​all,​(0)]_{=}$ Notation according to [[Classical Decision Problem]] classification:​ $[\exists^* \forall^*,​all,​(0)]_{=}$
Line 23: 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
 \] \]