Despite the title, the code on this page doesn't really prove rules, but rather checks whether they are tautologies. Practically, verifying that something is a tautology is equivalent to proving it in propositional calculus — you can do one if and only if you can do the other — but there is a huge principal difference between the two.
Richard Suchenwirth 2001-10-29: In Parsing Polish notation, it was shown how logical expressions in Polish notation can be translated to the more conventional special-character infix style. Another possibility is to translate them into the language expr understands: ECpqCNqNp is turned to (($p <= $q) == (!$q <= !$p)) For AND, OR, NOT we have && || !, equivalence is expressed with ==, and implication by <= (right-hand side is "at least as true" as left-hand side; note that this "arrow" seems to point the wrong way ;-). For completeness, J (!=) for XOR was added.
This way, we don't require special characters, but better still, we can let Tcl evaluate the value of an expression. And, iterating over all possible values for (in this case) p and q, we can find out whether the expression is always, sometimes, or never true. In the first case, we have a rule; also in the third, if we just negate it. The second case is definitely not a rule. So, here comes the modified translator:
proc polish2expr {polish} {
set s {}
foreach i [lrevert [split $polish ""]] {
switch -- $i {
A {push s "([pop s] || [pop s])"}
C {push s "([pop s] <= [pop s])"}
E {push s "([pop s] == [pop s])"}
J {push s "([pop s] != [pop s])"}
K {push s "([pop s] && [pop s])"}
N {push s "![pop s]"}
default {push s \$$i}
}
}
if {[llength $s]!=1} {error "bad PN, stack: $s"}
pop s
}
proc lrevert {list} {
set res {}
foreach i $list {set res [concat [list $i] $res]}
set res
}
proc push {name what} {upvar 1 $name s; lappend s $what}
proc pop {name} {
upvar 1 $name s
if ![llength $s] {error "bad PN, operand missing"}
set res [lindex $s end]
set s [lrange $s 0 end-1]
set res
}
if 0 {
Next we have to build the truth table, whose size depends on how many
variables are used. We need the list of variables anyway, so we define
each character that is not a PN operator ([[ACEJKN]]) to be a variable:
}
proc polishVariables {polish} {
# make a list of unique variables in PN expression
set res {}
foreach i [split $polish ""] {
if {![regexp $i ACEJKN] && [lsearch $res $i]<0} {
lappend res $i
}
}
set res
}
proc truthtable {n} {
# make a list of 2**n lists, each with n truth values 0|1
set res {}
for {set i 0} {$i < (1<<$n)} {incr i} {
set case {}
for {set j 0} {$j <$n} {incr j } {
lappend case [expr {($i & (1<<$j)) != 0}]
}
lappend res $case
}
lsort $res ;# just for better looks
}
if 0 {With these parts in place, building the prover is easy.
We collect the results as lists in two array elements, so we can
inspect cases that were neither true nor false:}
proc polishProve {polish} {
set expression [polish2expr $polish]
set variables [polishVariables $polish]
array set results {0 "" 1 ""}
foreach case [truthtable [llength $variables]] {
foreach $variables $case break ;# assign current values
lappend results([expr $expression!=0]) $case
}
if {$results(0)==""} {
return true
} elseif {$results(1)==""} {
return false
} else {
return "true only for ($variables): $results(1)"
}
}
if 0 {The simple error checking also allows to inspect what expression
is produced by a "Polish" input: just add a nonsense character to the end,
e.g.
% polishProve EKCpqCqpEpq.
bad PN, stack: {$.} {(($p <= $q) && ($q <= $p)) == ($p == $q)}
Or, it's not that much nonsense after all, considering that the "." command in Forth (see [RPN in Tcl]) means "print the stack"...
This may get boring, but I say it again: Is Tcl cool!}