12,080
edits
Changes
Directory:Jon Awbrey/Papers/Inquiry Driven Systems : Part 8 (view source)
Revision as of 18:00, 20 August 2011
, 18:00, 20 August 2011→8.3.2. “Study” : A Program for Reasoning with Propositions: + text
====8.3.2. “Study” : A Program for Reasoning with Propositions====
====8.3.2. “Study” : A Program for Reasoning with Propositions====
The "Study" module implements an inquiry driven system that helps the user reason with expressions in propositional calculus.
The "Model" function within this program is a generic routine that implements a type of interpreter for propositional calculus. It takes in a proposition expressed in a particular syntax for propositional calculus and generates a data structure that is tantamount to the Disjunctive Normal Form (DNF) of the proposition. I will use the function notation "DNF(P)" and "Model(P)" to indicate the output of this routine for the proposition P. The DNF of a proposition P, as expressed in the data structure Model(P), is in a sense the clearest expression of the proposition P relative to the particular class of purposes that are embodied in a given interpreter.
The Study module contains several functions which compute different kinds of normal forms for propositions. These procedures constitute "modelers" or "interpreters" of propositional syntax in the sense that they generate the logical "models" or satisfying "interpretations" of propositions.
Any procedure that computes a normal form exemplifies an important kind of inquiry driven system. The dimension of value, or motivation, associated with the process can be regarded as a measure of "clarity". In computing a normal form the interpreter passes from an arbitrary representation of an indicated objective, one that can be as obscure as possible within the bounds of acceptable syntax, to a standardized formulation, one that manifests a patently clear and readily readable expression of the same objective. Thus, the operation is one that preserves meaning while maximizing clarity and ease of application.
In computing a normal form the system passes from an arbitrarily obscure representation of a propositional objective to a maximally clear expression of the same objective.
Need to clarify that a normal form is defined relative to a particular class of purposes or questions. For example, a sorted list is a normal form for questions about the multiplicity of items on the list, that is, about the existence and the number of occurrences of given items on the list.
It needs to be understood that the cpncept of a canonical form is defined relative to a particular purpose, a purpose which is embodied in a particular interpreter, or which a particular interpreter is intended to realize. Often this purpose can be expressed as a task of answering a particular class of questions about the object domain.
For the purposes of this discussion, I will draw a distinction between "canonical forms" and "normal forms". Distinquish canonical form in a semantic equivalence class, the intentional concept, from normal form of a transformation, the operational concept. A canonical form is an expression that is especially well suited to represent its equivalence class. A normal form is a fixed point of a grammatical transformation, that is, a stable point of a rewrite procedure that acts on the space of expressions. When the intentional canon/ canonical intention is rendered operational/ put into operation by a particular interpreter, then the two notions coincide, but only then.
To illustrate how the Model program actualizes an inquiry process, I will treat two examples in detail, …
<pre>
Example 1: P(x, y) =
"x implies y".
Table 101.1 Standard Truth Table for P(x, y)
x y P
1 1 1
1 0 0
0 1 1
0 0 1
Table 101.2 Variant Truth Table for P(x, y)
P
x y 1
x (y) 0
(x) y 1
(x) (y) 1
Table 101.3 Model Tree for P(x, y)
___.____ x ___ y *
| |
| |____(y) -
|
|____(x)___ y *
|
|____(y) *
Table 102.1 Logical Input for P(x, y)
File: "P.log" Translation
( x ( y )) Not x without y.
Table 102.2 Model Output for P(x, y)
File: "P.mod" Model Value
x
y * *
(y ) - -
(x ) * *
Table 102.3 Tenor Output for P(x, y)
File: "P.ten" Model Count
x
y * 1
(x ) * 2
Table 102.4 Disjunctive Normal Form for P(x, y)
DNF Translation
(( x y Either x and y
)( ( x ) or not x
)) .
Table 103.1 Structure of the Sign Relation Rel(P)
Object Sign Interpretant
o1 s1 s2
o2 s1 s2
o3 s1 s2
o1 s2 s3
o2 s2 s3
o3 s2 s3
o1 s3 s3
o2 s3 s3
o3 s3 s3
Table 103.2 Contents of the Sign Relation Rel(P)
Element Description
o1 Point " x y " = <1, 1>
o2 Point "(x) y " = <0, 1>
o3 Point "(x)(y)" = <0, 0>
s1 Parse "(x (y))"
s2 Parse "(x y, (x))"
s3 Parse "(x (y, ()(y)), (x))"
Example 2: Q(x, y, z) =
"just one false of x, y, z".
Table 104.1 Standard Truth Table for Q(x, y, z)
x y z Q
1 1 1 0
1 1 0 1
1 0 1 1
1 0 0 0
0 1 1 1
0 1 0 0
0 0 1 0
0 0 0 0
Table 104.2 Variant Truth Table for Q(x, y, z)
Q
x y z 0
x y (z) 1
x (y) z 1
x (y) (z) 0
(x) y z 1
(x) y (z) 0
(x) (y) z 0
(x) (y) (z) 0
Table 104.3 Model Tree for Q(x, y, z)
___.____ x ___ y ___ z -
| | |
| | |____(z) *
| |
| |____(y)___ z *
| |
| |____(z) -
|
|____(x)___ y ___ z *
| |
| |____(z) -
|
|____(y)___ z -
|
|____(z) -
Table 105.1 Logical Input for Q(x, y, z)
File: "Q.log" Translation
( x , y , z ) Just one false
among x, y, z.
Table 105.2 Model Output for Q(x, y, z)
File: "Q.mod" Model Value
x
y
z - -
(z ) * *
(y )
z * *
(z ) - -
(x )
y
z * *
(z ) - -
(y ) - -
Table 105.3 Tenor Output for Q(x, y, z)
File: "Q.ten" Model Count
x
y
(z ) * 1
(y )
z * 2
(x )
y
z * 3
Table 105.4 Disjunctive Normal Form for Q(x, y, z)
DNF Translation
(( x y ( z ) Either x & y & -z
)( x ( y ) z or x & -y & z
)( ( x ) y z or -x & y & z
)) .
Table 106.1 Structure of the Sign Relation Rel(Q)
Object Sign Interpretant
o1 s1 s2
o2 s1 s2
o3 s1 s2
o1 s2 s3
o2 s2 s3
o3 s2 s3
o1 s3 s4
o2 s3 s4
o3 s3 s4
o1 s4 s4
o2 s4 s4
o3 s4 s4
Table 106.2 Contents of Rel(Q): Objects
Element Description
o1 Point " x y (z)" = <1, 1, 0>
o2 Point " x (y) z " = <1, 0, 1>
o3 Point "(x) y z " = <0, 1, 1>
Table 106.3 Contents of Rel(Q): Signs
Element Description
s1 Parse "(x, y, z)"
s2 Parse "( x (y, z)
,(x) y z
)"
s3 Parse "( x ( y (z)
,(y) z
)
,(x)( y z
,(y)()
)
)"
s4 Parse "( x ( y ( z ()
,(z) *
)
,(y)( z *
,(z)()
)
)
,(x)( y ( z *
,(z)()
)
,(y)()
)
)"
Table 107.1 Normal Form Expansion of Q(x, y, z): Version 1
Sign Expression Translation
s1 (x, y, z) Just one false of x, y, z
s2 ( x (y, z) Either x & (y, z)
,(x) y z or -x & y z
)
s3 ( x ( y (z) Either x & either y & (z)
,(y) z or -y & z
)
,(x)( y z or -x & either y & z
,(y)() or -y & false
)
)
s4 ( x ( y ( z () Either x & either y & either z & 0
,(z) * or -z & 1
)
,(y)( z * or -y & either z & 1
,(z)() or -z & 0
)
)
,(x)( y ( z * or -x & either y & either z & 1
,(z)() or -z & 0
)
,(y)() or -y & false
)
)
Table 107.2 Normal Form Expansion of Q(x, y, z): Version 2
Sign Expression Translation
s1 (x, y, z) Just one false of x, y, z.
s2 ( x (y, z) Either x & (y, z)
,(x) y z or not x & y z
) .
s3 ( x Either x &
( y (z) either y & (z)
,(y) z or not y & z
) ;
,(x) or not x &
( y z either y & z
,(y)() or not y & false
) ;
) .
s4 ( x Either x &
( y either y &
( z () either z & false
,(z) * or not z & true
) ;
,(y) or not y &
( z * either z & true
,(z)() or not z & false
) ;
) ;
,(x) or not x &
( y either y &
( z * either z & true
,(z)() or not z & false
) ;
,(y)() or not y & false
) ;
) .
</pre>
===8.4. Discussion and Development of Objectives===
===8.4. Discussion and Development of Objectives===