Difference between revisions of "Directory talk:Jon Awbrey/Papers/Propositional Equation Reasoning Systems"

MyWikiBiz, Author Your Legacy — Friday March 29, 2024
Jump to navigationJump to search
(document history)
 
(7 intermediate revisions by the same user not shown)
Line 1: Line 1:
==Document History==
+
==Place for Discussion==
  
===Standard Upper Ontology (Mar–Apr 2001)===
+
…
  
* http://suo.ieee.org/email/thrd186.html#04187
+
==Formal extension : Cactus calculus (Work Area)==
# http://suo.ieee.org/email/msg04187.html
 
# http://suo.ieee.org/email/msg04305.html
 
# http://suo.ieee.org/email/msg04413.html
 
# http://suo.ieee.org/email/msg04419.html
 
# http://suo.ieee.org/email/msg04422.html
 
# http://suo.ieee.org/email/msg04423.html
 
# http://suo.ieee.org/email/msg04432.html
 
# http://suo.ieee.org/email/msg04454.html
 
# http://suo.ieee.org/email/msg04455.html
 
# http://suo.ieee.org/email/msg04476.html
 
# http://suo.ieee.org/email/msg04510.html
 
# http://suo.ieee.org/email/msg04517.html
 
# http://suo.ieee.org/email/msg04525.html
 
# http://suo.ieee.org/email/msg04533.html
 
# http://suo.ieee.org/email/msg04536.html
 
# http://suo.ieee.org/email/msg04542.html
 
# http://suo.ieee.org/email/msg04546.html
 
  
===Ontology List (Mar–Apr 2001)===
+
Let us now extend the CSP–GSB calculus in the following way:
  
* http://suo.ieee.org/ontology/thrd74.html#01779
+
The first extension is the ''reflective extension of logical graphs'', or what may be described as the ''cactus language'', after its principal graph-theoretic data structure. It is generated by generalizing the negation operator <math>\texttt{(\_)}</math> in a particular manner, treating <math>\texttt{(\_)}</math> as the ''[[minimal negation operator]]'' of order 1, and adding another such operator for each integer parameter greater than 1. Taken in series, the minimal negation operators are symbolized by parenthesized argument lists of the following shapes: <math>\texttt{(\_)},</math>&nbsp; <math>\texttt{(\_, \_)},</math>&nbsp; <math>\texttt{(\_, \_, \_)},</math>&nbsp; and so on, where the number of argument slots is the order of the reflective negation operator in question.
# http://suo.ieee.org/ontology/msg01779.html
 
# http://suo.ieee.org/ontology/msg01897.html
 
# http://suo.ieee.org/ontology/msg02005.html
 
# http://suo.ieee.org/ontology/msg02011.html
 
# http://suo.ieee.org/ontology/msg02014.html
 
# http://suo.ieee.org/ontology/msg02015.html
 
# http://suo.ieee.org/ontology/msg02024.html
 
# http://suo.ieee.org/ontology/msg02046.html
 
# http://suo.ieee.org/ontology/msg02047.html
 
# http://suo.ieee.org/ontology/msg02068.html
 
# http://suo.ieee.org/ontology/msg02102.html
 
# http://suo.ieee.org/ontology/msg02109.html
 
# http://suo.ieee.org/ontology/msg02117.html
 
# http://suo.ieee.org/ontology/msg02125.html
 
# http://suo.ieee.org/ontology/msg02128.html
 
# http://suo.ieee.org/ontology/msg02134.html
 
# http://suo.ieee.org/ontology/msg02138.html
 
  
===Arisbe List (Feb 2003)===
+
===Cactus Language for Propositional Logic===
  
* http://stderr.org/pipermail/arisbe/2003-February/thread.html#1541
+
The development of differential logic is greatly facilitated by having a conceptually efficient calculus in place at the level of [[boolean-valued functions]] and elementary logical propositions. A calculus that is very efficient from both conceptual and computational standpoints is based on just two types of logical connectives, both of variable <math>k\!</math>-ary scope. The formulas of this calculus map into a species of graph-theoretical structures called ''painted and rooted cacti'' (PARCs) that lend visual representation to their functional structure and smooth the path to efficient computation.
# http://stderr.org/pipermail/arisbe/2003-February/001541.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001542.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001543.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001544.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001545.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001546.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001547.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001548.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001549.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001550.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001552.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001553.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001554.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001555.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001557.html
 
# http://stderr.org/pipermail/arisbe/2003-February/001559.html
 
  
===Ontology List (Feb 2003)===
+
{| align="center" cellpadding="6" width="90%"
 +
| The first kind of propositional expression is a parenthesized sequence of propositional expressions, written as <math>\texttt{(} e_1 \texttt{,} e_2 \texttt{,} \ldots \texttt{,} e_{k-1} \texttt{,} e_k \texttt{)}</math> and read to say that exactly one of the propositions <math>e_1, e_2, \ldots, e_{k-1}, e_k</math> is false, in other words, that their [[minimal negation]] is true.  A clause of this form maps into a PARC structure called a ''lobe'', in this case, one that is ''painted'' with the colors <math>e_1, e_2, \ldots, e_{k-1}, e_k</math> as shown below.
 +
|}
  
* http://suo.ieee.org/ontology/thrd19.html#04522
+
{| align="center" cellpadding="10"
* http://suo.ieee.org/ontology/thrd19.html#04532
+
| [[Image:Cactus Graph Lobe Connective.jpg|500px]]
# http://suo.ieee.org/ontology/msg04522.html
+
|}
# http://suo.ieee.org/ontology/msg04523.html
 
# http://suo.ieee.org/ontology/msg04524.html
 
# http://suo.ieee.org/ontology/msg04525.html
 
# http://suo.ieee.org/ontology/msg04526.html
 
# http://suo.ieee.org/ontology/msg04527.html
 
# http://suo.ieee.org/ontology/msg04528.html
 
# http://suo.ieee.org/ontology/msg04529.html
 
# http://suo.ieee.org/ontology/msg04530.html
 
# http://suo.ieee.org/ontology/msg04531.html
 
# http://suo.ieee.org/ontology/msg04532.html
 
# http://suo.ieee.org/ontology/msg04533.html
 
# http://suo.ieee.org/ontology/msg04534.html
 
# http://suo.ieee.org/ontology/msg04536.html
 
# http://suo.ieee.org/ontology/msg04537.html
 
# http://suo.ieee.org/ontology/msg04538.html
 
  
===Inquiry List (Mar 2003)===
+
{| align="center" cellpadding="6" width="90%"
 +
| The second kind of propositional expression is a concatenated sequence of propositional expressions, written as <math>e_1\ e_2\ \ldots\ e_{k-1}\ e_k</math> and read to say that all of the propositions <math>e_1, e_2, \ldots, e_{k-1}, e_k</math> are true, in other words, that their [[logical conjunction]] is true.  A clause of this form maps into a PARC structure called a ''node'', in this case, one that is ''painted'' with the colors <math>e_1, e_2, \ldots, e_{k-1}, e_k</math> as shown below.
 +
|}
  
* http://stderr.org/pipermail/inquiry/2003-March/thread.html#126
+
{| align="center" cellpadding="10"
# http://stderr.org/pipermail/inquiry/2003-March/000126.html
+
| [[Image:Cactus Graph Node Connective.jpg|500px]]
# http://stderr.org/pipermail/inquiry/2003-March/000127.html
+
|}
# http://stderr.org/pipermail/inquiry/2003-March/000128.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000129.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000130.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000131.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000132.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000133.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000134.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000135.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000136.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000137.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000138.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000139.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000140.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000141.html
 
# http://stderr.org/pipermail/inquiry/2003-March/000142.html
 
  
==Document History : Text File==
+
All other propositional connectives can be obtained through combinations of these two forms.  Strictly speaking, the parenthesized form is sufficient to define the concatenated form, making the latter formally dispensable, but it is convenient to maintain it as a concise way of expressing more complicated combinations of parenthesized forms.  While working with expressions solely in propositional calculus, it is easiest to use plain parentheses for logical connectives.  In contexts where ordinary parentheses are needed for other purposes an alternate typeface <math>\texttt{(} \ldots \texttt{)}</math> may be used for logical operators.
  
<pre>
+
Table&nbsp;1 collects a sample of basic propositional forms as expressed in terms of cactus language connectives.
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
  
Propositional Equation Reasoning Systems -- 2001
+
<br>
  
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
+
{| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:center; width:90%"
 +
|+ <math>\text{Table 1.}~~\text{Syntax and Semantics of a Calculus for Propositional Logic}</math>
 +
|- style="background:#f0f0ff"
 +
| <math>\text{Graph}\!</math>
 +
| <math>\text{Expression}\!</math>
 +
| <math>\text{Interpretation}\!</math>
 +
| <math>\text{Other Notations}\!</math>
 +
|-
 +
| height="100px" | [[Image:Rooted Node.jpg|20px]]
 +
| <math>~</math>
 +
| <math>\operatorname{true}</math>
 +
| <math>1\!</math>
 +
|-
 +
| height="100px" | [[Image:Rooted Edge.jpg|20px]]
 +
| <math>\texttt{(~)}</math>
 +
| <math>\operatorname{false}</math>
 +
| <math>0\!</math>
 +
|-
 +
| height="100px" | [[Image:Cactus A Big.jpg|20px]]
 +
| <math>a\!</math>
 +
| <math>a\!</math>
 +
| <math>a\!</math>
 +
|-
 +
| height="120px" | [[Image:Cactus (A) Big.jpg|20px]]
 +
| <math>\texttt{(} a \texttt{)}</math>
 +
| <math>\operatorname{not}~ a</math>
 +
| <math>\lnot a \quad \bar{a} \quad \tilde{a} \quad a^\prime</math>
 +
|-
 +
| height="100px" | [[Image:Cactus ABC Big.jpg|50px]]
 +
| <math>a ~ b ~ c</math>
 +
| <math>a ~\operatorname{and}~ b ~\operatorname{and}~ c</math>
 +
| <math>a \land b \land c</math>
 +
|-
 +
| height="160px" | [[Image:Cactus ((A)(B)(C)) Big.jpg|65px]]
 +
| <math>\texttt{((} a \texttt{)(} b \texttt{)(} c \texttt{))}</math>
 +
| <math>a ~\operatorname{or}~ b ~\operatorname{or}~ c</math>
 +
| <math>a \lor b \lor c</math>
 +
|-
 +
| height="120px" | [[Image:Cactus (A(B)) Big.jpg|60px]]
 +
| <math>\texttt{(} a \texttt{(} b \texttt{))}</math>
 +
|
 +
<math>\begin{matrix}
 +
a ~\operatorname{implies}~ b
 +
\\[6pt]
 +
\operatorname{if}~ a ~\operatorname{then}~ b
 +
\end{matrix}</math>
 +
| <math>a \Rightarrow b</math>
 +
|-
 +
| height="120px" | [[Image:Cactus (A,B) Big.jpg|65px]]
 +
| <math>\texttt{(} a \texttt{,} b \texttt{)}</math>
 +
|
 +
<math>\begin{matrix}
 +
a ~\operatorname{not~equal~to}~ b
 +
\\[6pt]
 +
a ~\operatorname{exclusive~or}~ b
 +
\end{matrix}</math>
 +
|
 +
<math>\begin{matrix}
 +
a \neq b
 +
\\[6pt]
 +
a + b
 +
\end{matrix}</math>
 +
|-
 +
| height="160px" | [[Image:Cactus ((A,B)) Big.jpg|65px]]
 +
| <math>\texttt{((} a \texttt{,} b \texttt{))}</math>
 +
|
 +
<math>\begin{matrix}
 +
a ~\operatorname{is~equal~to}~ b
 +
\\[6pt]
 +
a ~\operatorname{if~and~only~if}~ b
 +
\end{matrix}</math>
 +
|
 +
<math>\begin{matrix}
 +
a = b
 +
\\[6pt]
 +
a \Leftrightarrow b
 +
\end{matrix}</math>
 +
|-
 +
| height="120px" | [[Image:Cactus (A,B,C) Big.jpg|65px]]
 +
| <math>\texttt{(} a \texttt{,} b \texttt{,} c \texttt{)}</math>
 +
|
 +
<math>\begin{matrix}
 +
\operatorname{just~one~of}
 +
\\
 +
a, b, c
 +
\\
 +
\operatorname{is~false}.
 +
\end{matrix}</math>
 +
|
 +
<math>\begin{matrix}
 +
& \bar{a} ~ b ~ c
 +
\\
 +
\lor & a ~ \bar{b} ~ c
 +
\\
 +
\lor & a ~ b ~ \bar{c}
 +
\end{matrix}</math>
 +
|-
 +
| height="160px" | [[Image:Cactus ((A),(B),(C)) Big.jpg|65px]]
 +
| <math>\texttt{((} a \texttt{),(} b \texttt{),(} c \texttt{))}</math>
 +
|
 +
<math>\begin{matrix}
 +
\operatorname{just~one~of}
 +
\\
 +
a, b, c
 +
\\
 +
\operatorname{is~true}.
 +
\\[6pt]
 +
\operatorname{partition~all}
 +
\\
 +
\operatorname{into}~ a, b, c.
 +
\end{matrix}</math>
 +
|
 +
<math>\begin{matrix}
 +
& a ~ \bar{b} ~ \bar{c}
 +
\\
 +
\lor & \bar{a} ~ b ~ \bar{c}
 +
\\
 +
\lor & \bar{a} ~ \bar{b} ~ c
 +
\end{matrix}</math>
 +
|-
 +
| height="160px" | [[Image:Cactus (A,(B,C)) Big.jpg|90px]]
 +
| <math>\texttt{(} a \texttt{,(} b \texttt{,} c \texttt{))}</math>
 +
|
 +
<math>\begin{matrix}
 +
\operatorname{oddly~many~of}
 +
\\
 +
a, b, c
 +
\\
 +
\operatorname{are~true}.
 +
\end{matrix}</math>
 +
|
 +
<p><math>a + b + c\!</math></p>
 +
<br>
 +
<p><math>\begin{matrix}
 +
& a ~ b ~ c
 +
\\
 +
\lor & a ~ \bar{b} ~ \bar{c}
 +
\\
 +
\lor & \bar{a} ~ b ~ \bar{c}
 +
\\
 +
\lor & \bar{a} ~ \bar{b} ~ c
 +
\end{matrix}</math></p>
 +
|-
 +
| height="160px" | [[Image:Cactus (X,(A),(B),(C)) Big.jpg|90px]]
 +
| <math>\texttt{(} x \texttt{,(} a \texttt{),(} b \texttt{),(} c \texttt{))}</math>
 +
|
 +
<math>\begin{matrix}
 +
\operatorname{partition}~ x
 +
\\
 +
\operatorname{into}~ a, b, c.
 +
\\[6pt]
 +
\operatorname{genus}~ x ~\operatorname{comprises}
 +
\\
 +
\operatorname{species}~ a, b, c.
 +
\end{matrix}</math>
 +
|
 +
<math>\begin{matrix}
 +
& \bar{x} ~ \bar{a} ~ \bar{b} ~ \bar{c}
 +
\\
 +
\lor & x ~ a ~ \bar{b} ~ \bar{c}
 +
\\
 +
\lor & x ~ \bar{a} ~ b ~ \bar{c}
 +
\\
 +
\lor & x ~ \bar{a} ~ \bar{b} ~ c
 +
\end{matrix}</math>
 +
|}
  
PERS.  Propositional Equation Reasoning Systems
+
<br>
  
Version 1.  SUO List
+
The simplest expression for logical truth is the empty word, usually denoted by <math>\varepsilon\!</math> or <math>\lambda\!</math> in formal languages, where it forms the identity element for concatenation.  To make it visible in context, it may be denoted by the equivalent expression <math>{}^{\backprime\backprime} \texttt{((~))} {}^{\prime\prime},</math> or, especially if operating in an algebraic context, by a simple <math>{}^{\backprime\backprime} 1 {}^{\prime\prime}.</math>  Also when working in an algebraic mode, the plus sign <math>{}^{\backprime\backprime} + {}^{\prime\prime}</math> may be used for [[exclusive disjunction]]For example, we have the following paraphrases of algebraic expressions by means of parenthesized expressions:
  
01.  http://suo.ieee.org/email/msg04187.html
+
{| align="center" cellpadding="6" style="text-align:center"
02.  http://suo.ieee.org/email/msg04305.html
+
|
03.  http://suo.ieee.org/email/msg04413.html
+
<math>\begin{matrix}
04.  http://suo.ieee.org/email/msg04419.html
+
a + b
05.  http://suo.ieee.org/email/msg04422.html
+
& = &
06.  http://suo.ieee.org/email/msg04423.html
+
\texttt{(} a \texttt{,} b \texttt{)}
07.  http://suo.ieee.org/email/msg04432.html
+
\end{matrix}</math>
08.  http://suo.ieee.org/email/msg04454.html
+
|-
09.  http://suo.ieee.org/email/msg04455.html
+
|
10.  http://suo.ieee.org/email/msg04476.html
+
<math>\begin{matrix}
11.  http://suo.ieee.org/email/msg04510.html
+
a + b + c
12.  http://suo.ieee.org/email/msg04517.html
+
& = &
13.  http://suo.ieee.org/email/msg04525.html
+
\texttt{(} a \texttt{,(} b \texttt{,} c \texttt{))}
14.  http://suo.ieee.org/email/msg04533.html
+
& = &
15.  http://suo.ieee.org/email/msg04536.html
+
\texttt{((} a \texttt{,} b \texttt{),} c \texttt{)}
16.  http://suo.ieee.org/email/msg04542.html
+
\end{matrix}</math>
17.  http://suo.ieee.org/email/msg04546.html
+
|}
  
Version 1.  Ontology List
+
It is important to note that the last expressions are not equivalent to the 3-place parenthesis <math>\texttt{(} a \texttt{,} b \texttt{,} c \texttt{)}.</math>
 
 
01.  http://suo.ieee.org/ontology/msg01779.html
 
02.  http://suo.ieee.org/ontology/msg01897.html
 
03.  http://suo.ieee.org/ontology/msg02005.html
 
04.  http://suo.ieee.org/ontology/msg02011.html
 
05.  http://suo.ieee.org/ontology/msg02014.html
 
06.  http://suo.ieee.org/ontology/msg02015.html
 
07.  http://suo.ieee.org/ontology/msg02024.html
 
08.  http://suo.ieee.org/ontology/msg02046.html
 
09.  http://suo.ieee.org/ontology/msg02047.html
 
10.  http://suo.ieee.org/ontology/msg02068.html
 
11.  http://suo.ieee.org/ontology/msg02102.html
 
12.  http://suo.ieee.org/ontology/msg02109.html
 
13.  http://suo.ieee.org/ontology/msg02117.html
 
14.  http://suo.ieee.org/ontology/msg02125.html
 
15.  http://suo.ieee.org/ontology/msg02128.html
 
16.  http://suo.ieee.org/ontology/msg02134.html
 
17.  http://suo.ieee.org/ontology/msg02138.html
 
 
 
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
 
 
Propositional Equation Reasoning Systems -- 2003
 
 
 
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
 
 
PERS.  Propositional Equation Reasoning Systems
 
 
 
Version 2.  Ontology List
 
 
 
00.  http://suo.ieee.org/ontology/thrd19.html#04522
 
00.  http://suo.ieee.org/ontology/thrd19.html#04532
 
 
 
01.  http://suo.ieee.org/ontology/msg04522.html
 
02.  http://suo.ieee.org/ontology/msg04523.html
 
03.  http://suo.ieee.org/ontology/msg04524.html
 
04.  http://suo.ieee.org/ontology/msg04525.html
 
05.  http://suo.ieee.org/ontology/msg04526.html
 
06.  http://suo.ieee.org/ontology/msg04527.html
 
07.  http://suo.ieee.org/ontology/msg04528.html
 
08.  http://suo.ieee.org/ontology/msg04529.html
 
09.  http://suo.ieee.org/ontology/msg04530.html
 
10.  http://suo.ieee.org/ontology/msg04531.html
 
11.  http://suo.ieee.org/ontology/msg04532.html
 
12.  http://suo.ieee.org/ontology/msg04533.html
 
13.  http://suo.ieee.org/ontology/msg04534.html
 
14.  http://suo.ieee.org/ontology/msg04536.html
 
15.  http://suo.ieee.org/ontology/msg04537.html
 
16.  http://suo.ieee.org/ontology/msg04538.html
 
 
 
Version 2.  Arisbe List
 
 
 
01.  http://stderr.org/pipermail/arisbe/2003-February/001541.html
 
02.  http://stderr.org/pipermail/arisbe/2003-February/001542.html
 
03.  http://stderr.org/pipermail/arisbe/2003-February/001543.html
 
04.  http://stderr.org/pipermail/arisbe/2003-February/001544.html
 
05.  http://stderr.org/pipermail/arisbe/2003-February/001545.html
 
06.  http://stderr.org/pipermail/arisbe/2003-February/001546.html
 
07.  http://stderr.org/pipermail/arisbe/2003-February/001547.html
 
08.  http://stderr.org/pipermail/arisbe/2003-February/001548.html
 
09.  http://stderr.org/pipermail/arisbe/2003-February/001549.html
 
10.  http://stderr.org/pipermail/arisbe/2003-February/001550.html
 
11.  http://stderr.org/pipermail/arisbe/2003-February/001552.html
 
12.  http://stderr.org/pipermail/arisbe/2003-February/001553.html
 
13.  http://stderr.org/pipermail/arisbe/2003-February/001554.html
 
14.  http://stderr.org/pipermail/arisbe/2003-February/001555.html
 
15.  http://stderr.org/pipermail/arisbe/2003-February/001557.html
 
16.  http://stderr.org/pipermail/arisbe/2003-February/001559.html
 
 
 
Version 3.  Inquiry List
 
 
 
00.  http://stderr.org/pipermail/inquiry/2003-March/thread.html#126
 
01.  http://stderr.org/pipermail/inquiry/2003-March/000126.html
 
02.  http://stderr.org/pipermail/inquiry/2003-March/000127.html
 
03.  http://stderr.org/pipermail/inquiry/2003-March/000128.html
 
04.  http://stderr.org/pipermail/inquiry/2003-March/000129.html
 
05.  http://stderr.org/pipermail/inquiry/2003-March/000130.html
 
06.  http://stderr.org/pipermail/inquiry/2003-March/000131.html
 
07.  http://stderr.org/pipermail/inquiry/2003-March/000132.html
 
08.  http://stderr.org/pipermail/inquiry/2003-March/000133.html
 
09.  http://stderr.org/pipermail/inquiry/2003-March/000134.html
 
10.  http://stderr.org/pipermail/inquiry/2003-March/000135.html
 
11.  http://stderr.org/pipermail/inquiry/2003-March/000136.html
 
12.  http://stderr.org/pipermail/inquiry/2003-March/000137.html
 
13.  http://stderr.org/pipermail/inquiry/2003-March/000138.html
 
14.  http://stderr.org/pipermail/inquiry/2003-March/000139.html
 
15.  http://stderr.org/pipermail/inquiry/2003-March/000140.html
 
16.  http://stderr.org/pipermail/inquiry/2003-March/000141.html
 
17.  http://stderr.org/pipermail/inquiry/2003-March/000142.html
 
 
 
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
 
 
Propositional Equation Reasoning Systems -- 2004-2006
 
 
 
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
 
 
PERS.  Propositional Equation Reasoning Systems
 
 
 
Version 4.  NKS Forum
 
 
 
00.  http://forum.wolframscience.com/showthread.php?threadid=297
 
01.  http://forum.wolframscience.com/showthread.php?postid=950#post950
 
02.  http://forum.wolframscience.com/showthread.php?postid=952#post952
 
03.  http://forum.wolframscience.com/showthread.php?postid=953#post953
 
04.  http://forum.wolframscience.com/showthread.php?postid=954#post954
 
05.  http://forum.wolframscience.com/showthread.php?postid=957#post957
 
06.  http://forum.wolframscience.com/showthread.php?postid=958#post958
 
07.  http://forum.wolframscience.com/showthread.php?postid=959#post959
 
08.  http://forum.wolframscience.com/showthread.php?postid=961#post961
 
09.  http://forum.wolframscience.com/showthread.php?postid=962#post962
 
10.  http://forum.wolframscience.com/showthread.php?postid=964#post964
 
11.  http://forum.wolframscience.com/showthread.php?postid=965#post965
 
12.  http://forum.wolframscience.com/showthread.php?postid=967#post967
 
13.  http://forum.wolframscience.com/showthread.php?postid=968#post968
 
14.  http://forum.wolframscience.com/showthread.php?postid=973#post973
 
15.  http://forum.wolframscience.com/showthread.php?postid=976#post976
 
16.  http://forum.wolframscience.com/showthread.php?postid=977#post977
 
17.  http://forum.wolframscience.com/showthread.php?postid=981#post981
 
18.  http://forum.wolframscience.com/showthread.php?postid=988#post988
 
19.  http://forum.wolframscience.com/showthread.php?postid=990#post990
 
20.  http://forum.wolframscience.com/showthread.php?postid=994#post994
 
21.  http://forum.wolframscience.com/showthread.php?postid=1003#post1003
 
22.  http://forum.wolframscience.com/showthread.php?postid=1005#post1005
 
23.  http://forum.wolframscience.com/showthread.php?postid=1015#post1015
 
24.  http://forum.wolframscience.com/showthread.php?postid=1022#post1022
 
25.  http://forum.wolframscience.com/showthread.php?postid=1025#post1025
 
26.  http://forum.wolframscience.com/showthread.php?postid=1031#post1031
 
27.  http://forum.wolframscience.com/showthread.php?postid=1220#post1220
 
28.  http://forum.wolframscience.com/showthread.php?postid=1224#post1224
 
29.  http://forum.wolframscience.com/showthread.php?postid=1227#post1227
 
30.  http://forum.wolframscience.com/showthread.php?postid=1228#post1228
 
31.  http://forum.wolframscience.com/showthread.php?postid=1232#post1232
 
32.  http://forum.wolframscience.com/showthread.php?postid=1249#post1249
 
33.  http://forum.wolframscience.com/showthread.php?postid=1262#post1262
 
34.  http://forum.wolframscience.com/showthread.php?postid=1265#post1265
 
35.  http://forum.wolframscience.com/showthread.php?postid=1273#post1273
 
36.
 
 
 
Version 4.  Inquiry List
 
 
 
00.  http://stderr.org/pipermail/inquiry/2004-April/thread.html#1341
 
00.  http://stderr.org/pipermail/inquiry/2004-May/thread.html#1391
 
00.  http://stderr.org/pipermail/inquiry/2006-January/thread.html#3364
 
 
 
01.  http://stderr.org/pipermail/inquiry/2004-April/001341.html
 
02.  http://stderr.org/pipermail/inquiry/2004-April/001342.html
 
03.  http://stderr.org/pipermail/inquiry/2004-April/001343.html
 
04.  http://stderr.org/pipermail/inquiry/2004-April/001344.html
 
05.  http://stderr.org/pipermail/inquiry/2004-April/001345.html
 
06.  http://stderr.org/pipermail/inquiry/2004-April/001346.html
 
07.  http://stderr.org/pipermail/inquiry/2004-April/001347.html
 
08.  http://stderr.org/pipermail/inquiry/2004-April/001348.html
 
09.  http://stderr.org/pipermail/inquiry/2004-April/001349.html
 
10.  http://stderr.org/pipermail/inquiry/2004-April/001350.html
 
11.  http://stderr.org/pipermail/inquiry/2004-April/001351.html
 
12.  http://stderr.org/pipermail/inquiry/2004-April/001352.html
 
13.  http://stderr.org/pipermail/inquiry/2004-April/001353.html
 
14.  http://stderr.org/pipermail/inquiry/2004-April/001354.html
 
15.  http://stderr.org/pipermail/inquiry/2004-April/001355.html
 
16.  http://stderr.org/pipermail/inquiry/2004-April/001356.html
 
17.  http://stderr.org/pipermail/inquiry/2004-April/001357.html
 
18.  http://stderr.org/pipermail/inquiry/2004-April/001358.html
 
19.  http://stderr.org/pipermail/inquiry/2004-April/001359.html
 
20.  http://stderr.org/pipermail/inquiry/2004-April/001360.html
 
21.  http://stderr.org/pipermail/inquiry/2004-April/001361.html
 
22.  http://stderr.org/pipermail/inquiry/2004-April/001362.html
 
23.  http://stderr.org/pipermail/inquiry/2004-April/001363.html
 
24.  http://stderr.org/pipermail/inquiry/2004-April/001364.html
 
25.  http://stderr.org/pipermail/inquiry/2004-April/001365.html
 
26.  http://stderr.org/pipermail/inquiry/2004-April/001366.html
 
27.  http://stderr.org/pipermail/inquiry/2004-April/001389.html
 
28.  http://stderr.org/pipermail/inquiry/2004-April/001390.html
 
29.  http://stderr.org/pipermail/inquiry/2004-May/001391.html
 
30.  http://stderr.org/pipermail/inquiry/2004-May/001392.html
 
31.  http://stderr.org/pipermail/inquiry/2004-May/001393.html
 
32.  http://stderr.org/pipermail/inquiry/2004-May/001394.html
 
33.  http://stderr.org/pipermail/inquiry/2004-May/001395.html
 
34.  http://stderr.org/pipermail/inquiry/2004-May/001396.html
 
35.  http://stderr.org/pipermail/inquiry/2004-May/001398.html
 
36.  http://stderr.org/pipermail/inquiry/2006-January/003364.html
 
37.
 
 
 
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
</pre>
 

Latest revision as of 03:28, 1 October 2010

Place for Discussion

Formal extension : Cactus calculus (Work Area)

Let us now extend the CSP–GSB calculus in the following way:

The first extension is the reflective extension of logical graphs, or what may be described as the cactus language, after its principal graph-theoretic data structure. It is generated by generalizing the negation operator \(\texttt{(\_)}\) in a particular manner, treating \(\texttt{(\_)}\) as the minimal negation operator of order 1, and adding another such operator for each integer parameter greater than 1. Taken in series, the minimal negation operators are symbolized by parenthesized argument lists of the following shapes\[\texttt{(\_)},\]  \(\texttt{(\_, \_)},\)  \(\texttt{(\_, \_, \_)},\)  and so on, where the number of argument slots is the order of the reflective negation operator in question.

Cactus Language for Propositional Logic

The development of differential logic is greatly facilitated by having a conceptually efficient calculus in place at the level of boolean-valued functions and elementary logical propositions. A calculus that is very efficient from both conceptual and computational standpoints is based on just two types of logical connectives, both of variable \(k\!\)-ary scope. The formulas of this calculus map into a species of graph-theoretical structures called painted and rooted cacti (PARCs) that lend visual representation to their functional structure and smooth the path to efficient computation.

The first kind of propositional expression is a parenthesized sequence of propositional expressions, written as \(\texttt{(} e_1 \texttt{,} e_2 \texttt{,} \ldots \texttt{,} e_{k-1} \texttt{,} e_k \texttt{)}\) and read to say that exactly one of the propositions \(e_1, e_2, \ldots, e_{k-1}, e_k\) is false, in other words, that their minimal negation is true. A clause of this form maps into a PARC structure called a lobe, in this case, one that is painted with the colors \(e_1, e_2, \ldots, e_{k-1}, e_k\) as shown below.
Cactus Graph Lobe Connective.jpg
The second kind of propositional expression is a concatenated sequence of propositional expressions, written as \(e_1\ e_2\ \ldots\ e_{k-1}\ e_k\) and read to say that all of the propositions \(e_1, e_2, \ldots, e_{k-1}, e_k\) are true, in other words, that their logical conjunction is true. A clause of this form maps into a PARC structure called a node, in this case, one that is painted with the colors \(e_1, e_2, \ldots, e_{k-1}, e_k\) as shown below.
Cactus Graph Node Connective.jpg

All other propositional connectives can be obtained through combinations of these two forms. Strictly speaking, the parenthesized form is sufficient to define the concatenated form, making the latter formally dispensable, but it is convenient to maintain it as a concise way of expressing more complicated combinations of parenthesized forms. While working with expressions solely in propositional calculus, it is easiest to use plain parentheses for logical connectives. In contexts where ordinary parentheses are needed for other purposes an alternate typeface \(\texttt{(} \ldots \texttt{)}\) may be used for logical operators.

Table 1 collects a sample of basic propositional forms as expressed in terms of cactus language connectives.


\(\text{Table 1.}~~\text{Syntax and Semantics of a Calculus for Propositional Logic}\)
\(\text{Graph}\!\) \(\text{Expression}\!\) \(\text{Interpretation}\!\) \(\text{Other Notations}\!\)
Rooted Node.jpg \(~\) \(\operatorname{true}\) \(1\!\)
Rooted Edge.jpg \(\texttt{(~)}\) \(\operatorname{false}\) \(0\!\)
Cactus A Big.jpg \(a\!\) \(a\!\) \(a\!\)
Cactus (A) Big.jpg \(\texttt{(} a \texttt{)}\) \(\operatorname{not}~ a\) \(\lnot a \quad \bar{a} \quad \tilde{a} \quad a^\prime\)
Cactus ABC Big.jpg \(a ~ b ~ c\) \(a ~\operatorname{and}~ b ~\operatorname{and}~ c\) \(a \land b \land c\)
Cactus ((A)(B)(C)) Big.jpg \(\texttt{((} a \texttt{)(} b \texttt{)(} c \texttt{))}\) \(a ~\operatorname{or}~ b ~\operatorname{or}~ c\) \(a \lor b \lor c\)
Cactus (A(B)) Big.jpg \(\texttt{(} a \texttt{(} b \texttt{))}\)

\(\begin{matrix} a ~\operatorname{implies}~ b \\[6pt] \operatorname{if}~ a ~\operatorname{then}~ b \end{matrix}\)

\(a \Rightarrow b\)
Cactus (A,B) Big.jpg \(\texttt{(} a \texttt{,} b \texttt{)}\)

\(\begin{matrix} a ~\operatorname{not~equal~to}~ b \\[6pt] a ~\operatorname{exclusive~or}~ b \end{matrix}\)

\(\begin{matrix} a \neq b \\[6pt] a + b \end{matrix}\)

Cactus ((A,B)) Big.jpg \(\texttt{((} a \texttt{,} b \texttt{))}\)

\(\begin{matrix} a ~\operatorname{is~equal~to}~ b \\[6pt] a ~\operatorname{if~and~only~if}~ b \end{matrix}\)

\(\begin{matrix} a = b \\[6pt] a \Leftrightarrow b \end{matrix}\)

Cactus (A,B,C) Big.jpg \(\texttt{(} a \texttt{,} b \texttt{,} c \texttt{)}\)

\(\begin{matrix} \operatorname{just~one~of} \\ a, b, c \\ \operatorname{is~false}. \end{matrix}\)

\(\begin{matrix} & \bar{a} ~ b ~ c \\ \lor & a ~ \bar{b} ~ c \\ \lor & a ~ b ~ \bar{c} \end{matrix}\)

Cactus ((A),(B),(C)) Big.jpg \(\texttt{((} a \texttt{),(} b \texttt{),(} c \texttt{))}\)

\(\begin{matrix} \operatorname{just~one~of} \\ a, b, c \\ \operatorname{is~true}. \\[6pt] \operatorname{partition~all} \\ \operatorname{into}~ a, b, c. \end{matrix}\)

\(\begin{matrix} & a ~ \bar{b} ~ \bar{c} \\ \lor & \bar{a} ~ b ~ \bar{c} \\ \lor & \bar{a} ~ \bar{b} ~ c \end{matrix}\)

Cactus (A,(B,C)) Big.jpg \(\texttt{(} a \texttt{,(} b \texttt{,} c \texttt{))}\)

\(\begin{matrix} \operatorname{oddly~many~of} \\ a, b, c \\ \operatorname{are~true}. \end{matrix}\)

\(a + b + c\!\)


\(\begin{matrix} & a ~ b ~ c \\ \lor & a ~ \bar{b} ~ \bar{c} \\ \lor & \bar{a} ~ b ~ \bar{c} \\ \lor & \bar{a} ~ \bar{b} ~ c \end{matrix}\)

Cactus (X,(A),(B),(C)) Big.jpg \(\texttt{(} x \texttt{,(} a \texttt{),(} b \texttt{),(} c \texttt{))}\)

\(\begin{matrix} \operatorname{partition}~ x \\ \operatorname{into}~ a, b, c. \\[6pt] \operatorname{genus}~ x ~\operatorname{comprises} \\ \operatorname{species}~ a, b, c. \end{matrix}\)

\(\begin{matrix} & \bar{x} ~ \bar{a} ~ \bar{b} ~ \bar{c} \\ \lor & x ~ a ~ \bar{b} ~ \bar{c} \\ \lor & x ~ \bar{a} ~ b ~ \bar{c} \\ \lor & x ~ \bar{a} ~ \bar{b} ~ c \end{matrix}\)


The simplest expression for logical truth is the empty word, usually denoted by \(\varepsilon\!\) or \(\lambda\!\) in formal languages, where it forms the identity element for concatenation. To make it visible in context, it may be denoted by the equivalent expression \({}^{\backprime\backprime} \texttt{((~))} {}^{\prime\prime},\) or, especially if operating in an algebraic context, by a simple \({}^{\backprime\backprime} 1 {}^{\prime\prime}.\) Also when working in an algebraic mode, the plus sign \({}^{\backprime\backprime} + {}^{\prime\prime}\) may be used for exclusive disjunction. For example, we have the following paraphrases of algebraic expressions by means of parenthesized expressions:

\(\begin{matrix} a + b & = & \texttt{(} a \texttt{,} b \texttt{)} \end{matrix}\)

\(\begin{matrix} a + b + c & = & \texttt{(} a \texttt{,(} b \texttt{,} c \texttt{))} & = & \texttt{((} a \texttt{,} b \texttt{),} c \texttt{)} \end{matrix}\)

It is important to note that the last expressions are not equivalent to the 3-place parenthesis \(\texttt{(} a \texttt{,} b \texttt{,} c \texttt{)}.\)