12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Saturday May 04, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Inquiry Driven Systems : Part 8 (view source)
Revision as of 16:34, 26 June 2013
, 16:34, 26 June 2013no edit summary
====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===
====8.4.1. Objective 1a : Propositions as Types====
====8.4.1. Objective 1a : Propositions as Types====
In this component I investigate an important relationship that exists between two kinds of formal systems, called applicational calculi (AC's) and propositional calculi (PC's).
Expressions in an applicational calculus are called "terms" and are built up from a supply of primitive symbols called "basic terms" through the use of a binary operation called "application".
Expressions in a propositional calculus are called "propositions" and are built up from a supply of primitive symbols called "basic propositions" through the use of a stock of k ary operations called "connectives".
Exact formalization of symbolic calculi is absolutely necessary, especially if we want computers to serve as interpreters, or at least to lighten the burdens of interpretation by taking up the bit parts of formal routines. Because the problem environments where calculi develop show no signs of stopping in their growing complexity, it becomes inevitable that we turn to computers as auxiliary interpreters of formal systems, to secure their operational significance and manage the increasing complications of their practical use. But a formalized syntax, however necessary, is not enough to demonstrate utility.
A calculus is never a finished object, complete in itself, but a tool shaped to the end of interpretation.
I am using the word "interpretation" to denote the whole complex of activities through which signs acquire practical meaning. For human beings the process of interpretation is a largely automatic and usually unanalyzed affair, but it can also be highly flexible and unusually adaptive. Human language users or symbol manipulators have powers they hardly reflect on and barely understand, to entertain novel associations between signs and whatever it is that signs convey, to examine habitual assumptions about the meaning of symbols in practice.
One person can simply invite another to entertain new associations between signs and ideas or to examine old assumptions about their meaning in practice, and the other is somehow able to comply, if only for the sake of experiment and argument. But the need to supply a formal system with a computational basis, involving exact syntax, effective semantics, and computerized "pragmatics" (that is, a computer supported operational basis) requires us to analyze the process of interpretation in minute detail and on new grounds.
In use, AC's and PC's take on meaning according to a variety of interpretive rules. I am adopting an interpretation on either side that highlights the relation of interest between these two kinds of calculi and that brings the intended correspondence into sharper relief.
In both kinds of calculus the primitive symbols are distinguished as "constants" and "variables". A constant is a name for a definite object of thought, and is intended to maintain a fixed meaning throughout a given discussion. A variable is a symbol of indefinite reference, or a token without a pre assigned meaning, but is used as a site for the substitution of other expressions or as a placeholder for a multitude of conceptual objects and logical values.
Semantics. Meanings are provided or attached to symbols by means of:
1. Contexts of occurrence: the facts or rules of distribution.
2. Action induced on other symbols by means of rewrite rules:
:: generators and relations, or paraphrastic definitions.
3. Synonymy: membership in semantic equivalence classes.
4. Arbitrary fiat, external designation, or special convention.
====8.4.2. Objective 1b : Proof Styles and Developments====
====8.4.2. Objective 1b : Proof Styles and Developments====
</div>
</div>
----
----
[[Category:Artificial Intelligence]]
[[Category:Artificial Intelligence]]
