Differences
This shows you the differences between two versions of the page.
horn_formulas [2010/08/18 12:35] jipsen |
horn_formulas [2017/10/01 20:07] (current) jipsen |
||
---|---|---|---|
Line 1: | Line 1: | ||
[[Syntax]] | [[Terms]] | [[Equations]] | [[Horn formulas]] | [[Universal formulas]] | [[First-order formulas]] | [[Theories]] | [[Syntax]] | [[Terms]] | [[Equations]] | [[Horn formulas]] | [[Universal formulas]] | [[First-order formulas]] | [[Theories]] | ||
- | A list of quasiequations and universal Horn formulas. | + | A list of atomic formulas, quasiequations and universal Horn formulas. |
+ | |reflexive: | $xRx$ ||| | ||
|transitive: | $xRy \mbox{ and } yRz\Longrightarrow xRz$ ||| | |transitive: | $xRy \mbox{ and } yRz\Longrightarrow xRz$ ||| | ||
|antisymmetric: | $xRy \mbox{ and } yRx\Longrightarrow x=y$ ||| | |antisymmetric: | $xRy \mbox{ and } yRx\Longrightarrow x=y$ ||| | ||
|left cancellation: | $x*y=x*z\Longrightarrow y=z$ | right cancellation: | $x*z=y*z\Longrightarrow x=y$ | | |left cancellation: | $x*y=x*z\Longrightarrow y=z$ | right cancellation: | $x*z=y*z\Longrightarrow x=y$ | | ||
+ | |left R-preserving: | $xRy \Longrightarrow z*x\ R\ z*y$ | right R-preserving: | $xRy \Longrightarrow x*z\ R\ y*z$ | |
Trace: