#!/usr/bin/perl
print "Content-type: text/html\n\n";
### DEFINE SPECIAL CHARACTERS: carriage return, line feed, blank, etc.;
$cr=chr(13); $lf=chr(10); $bk=chr(32); $pl="+";
$crlf=join('',$cr,$lf);
### CAPTURE TODAY'S DATE, QUERY, AND ADDRESSES FROM ENVIRONMENTAL VARIABLES.
$tdate=`date`; chop($tdate); $taddr=$ENV{'REMOTE_ADDR'};
###
### PRINT HEADER.
print qq|Live Nandset Theorem Prover. 2/17/2008.|;
print qq|\n|;
print qq|\nLIVE NANDSET THEOREM PROVER. 2/17/2008.
|;
print qq|\n
$tdate |;
###
### INITIALIZE VARIABLES.
$inputbox=""; $outputbox=""; $nline=0; $iline=0; $jline=0; $kline=0;
$vacusw=0; $cntrsw=0; $nline=0; $nname=0; $firstline=1;
###
### CAPTURE INPUTBOX.
$inb=; ($scr,$inputbox)=split(/text=/,$inb,2);
###
### TRANSLATE INTO OUTPUTBOX: REMOVE ESCAPE SEQUENCES.
$oub=$inputbox; $oub=~s/\+/$bk/g; $oub=~s/%2B/\+/g; $oub=~s/%3A/\:/g;
$oub=~s/%3D/\=/g; $oub=~s/%5E/\^/g; $oub=~s/%24/\$/g; $oub=~s/%21/\!/g;
$oub=~s/%23/\#/g; $oub=~s/%26/\&/g; $oub=~s/%0D%0A/$crlf/g;
$oubx=join('',$oub,$crlf,$crlf); $outputbox=$oubx;
$lcoutputbox=lc($outputbox);
@dtbox=split(/$lf/,$lcoutputbox); $ndtbox=@dtbox; $splitbox=$ndtbox+4;
###
### INITIALIZE PARENTS, VACUITIES, CONTRADICTIONS, CARDINALITIES, NANDSETS.
$iline=-1; while($iline<$splitbox){$iline++; $parnt[$iline]=0;
$sibln[$iline]=0; $gprnt[$iline]=0; $slabl[$iline]="";
$fchld[$iline]=0; $logel[$iline]=0; $dtsrc[$iline]=0; $isfch[$iline]=0;
$cardn[$iline]=0; $contr[$iline]=0; $vacus[$iline]=1; $solun[$iline]=0;
$nands[$iline][1]=1;
$jline=1; while($jline<$mxcol){$jline++; $nands[$iline][$jline]=0;};};
$parnt[1]=1; $sign[1]=1; $nands[1][1]=1;
###
### PARSE OUTPUTBOX
$idtbox=-1;
while($idtbox<$ndtbox){$idtbox++; $tbox0=$dtbox[$idtbox]; chop($tbox0);
($tbox1,$tbox2)=split(/\:/,$tbox0,2); if($tbox2 eq ""){$tbox2=$tbox1;};
($tbox3,$tbox4)=split(/\^/,$tbox2,2);
$tbox=$tbox3; $pbox=$idtsrc+1; $bot=""; $top=""; $lnb=0; $sgn=0; $col=0;
###
### IF OUTPUTLINE IS SEPARATED BY + OR -...
$splpl=split(/\+/,$tbox); $splmn=split(/\-/,$tbox);
if($splpl>1){($bot,$top)=split(/\+/,$tbox); $lnb=length($bot); $sgn=1;};
if($splmn>1){($bot,$top)=split(/\-/,$tbox); $lnb=length($bot); $sgn=-1;};
if($lnb>0){if($sgn!=0){$col=($lnb+2)/3; $nline++; $tnm=0;
$dtsrc[$nline]=$tbox; $clmn[$nline]=$col; $sign[$nline]=$sgn;
###
### IF THE NAME IS ALREADY DEFINED...
if(defined($eman{$top})){$tnm=$eman{$top};};
###
### INCLUDE NEW NAME.
if($tnm<1){$nname++; $tnm=$nname; $name[$tnm]=$top;
$eman{$top}=$nname;}; $logel[$nline]=$tnm;
$chlog[$nline]=$top;};};};
###
### PRINT PARSED OUTPUTBOX
$iline=0; while($iline<$nline){$iline++; $sgn=$sign[$iline];
$col=$clmn[$iline]; $nml=$logel[$iline]; $top=$name[$nml];};
###
### FIND MAX COLUMN NUMBER, $mxcol.
$mxcol=0; $iline=0; while($iline<$nline){$iline++; $col=$clmn[$iline];
if($col>$mxcol){$mxcol=$col;};};
###
### FIND PARENTS.
$vacusw=0; $cntrsw=0; $iline=0;
while($iline<$nline){$iline++; $cli=$clmn[$iline]; $clp=$cli+1;
$jline=$iline; $jstop=0;
while(($jline<$nline)&&($jstop<1)){$jline++; $clj=$clmn[$jline];
if($clj<$clp){$jstop=1;}; if($jstop<1){$parnt[$jline]=$iline;};};};
###
### CALCULATE FIRST_CHILDREN.
$iline=1; while($iline<$nline){$iline++; $pline=$parnt[$iline];
$fchlp=$fchld[$pline]; if($fchlp<1){$fchld[$pline]=$iline;};};
###
### INITIALIZE SIBLINGS, PARENTS.
$iline=1; while($iline<$nline){$iline++; $pline=$parnt[$iline]; $xline=-1;
while($xline<$nline){$xline++; $sibln[$xline]=0; $gprnt[$xline]=0;
$nands[$iline][$xline]=0;};
$fchlp=$fchld[$pline]; if($fchlp==$iline){
$kline=1; while($kline<$nline){$kline++; $rline=$parnt[$kline];
if($pline==$rline){$sibln[$kline]=$fchlp;};};
###
### CALCULATE GRANDPARENTS.
$gprlk=$pline; $kline=0; while($kline<$iline){$kline++;
$gprnt[$gprlk]=$iline; if($gprlk>1){$gprlk=$parnt[$gprlk];};};
###
### CALCULATE VACUITIES.
$vacus[$iline]=0;
$kline=0; while($kline<$nline){$kline++;
$signk=0; $logek=0;
$gprnk=$gprnt[$kline]; $siblk=$sibln[$kline];
if($gprnk==$iline){$signk=$sign[$kline]; $logek=$logel[$kline];};
if($siblk==$iline){$signk=0-$sign[$kline]; $logek=$logel[$kline];};
$signm=0-$signk;
if($logek>0){$nandk=$nands[$iline][$logek];
if($nandk==$signm){$vacus[$iline]=1;};
if($nandk!=$signm){$nands[$iline][$logek]=$signk;};};};};};
###
### CALCULATE VACUITY SWITCH.
$vacusw=1;
$iline=1; while($iline<$nline){$iline++; $pline=$parnt[$iline];
$fchlp=$fchld[$pline]; if($fchlp==$iline){
if($vacus[$iline]<1){$vacusw=0;};};};
###
### INPUT POST METHOD.
print qq|\n
|;
###
### THEOREM IS VACUOUS.
if($vacusw>0){print "\n
Theorem is vacuous.
";};
###
### THEOREM IS NON-VACUOUS.
if($vacusw<1){print "\n
Theorem is non-vacuous:";
###
### CALCULATE CARDINALITY.
$cntrsw=0; $iline=1;
while($iline<$nline){$iline++; $vacui=$vacus[$iline]; $cardi=0;
if($vacui<1){$jname=1;
while($jname<$nname){$jname++; $signj=$nands[$iline][$jname];
if($signj!=0){$cardi++;};};}; $cardn[$iline]=$cardi;};
###
### CALCULATE INITIAL SOLUTIONS.
$iline=1; while($iline<$nline){$iline++; $vacui=$vacus[$iline];
if($vacui<1){$cardi=$cardn[$iline]; if($cardi==1){$jname=1;
while($jname<$nname){$jname++; $signj=$nands[$iline][$jname];
if($signj!=0){$solui=$jname*$signj; $solun[$iline]=$solui;
if($signj==1){$plmn="-";}; if($signj==-1){$plmn="+";};
$nmslj=join('',$plmn,$name[$jname]);
$slabl[$iline]=$nmslj;};};};};};
###
### PRINT INITIAL SOLUTIONS.
print "\n
Initial solutions:";
$iline=1; while($iline<$nline){$iline++; $solui=$solun[$iline];
if($solui!=0){$slabi=$slabl[$iline]; print " $slabi";};};
###
### CALCULATE ADDITIONAL SOLUTIONS.
print "\n
Additional solutions:";
if($cntrsw<1){
$iline=1; while($iline<$nline){$iline++; $solui=$solun[$iline];
if($solui!=0){if($solui>0){$signi=1;}; if($solui<0){$signi=-1;};
$signm=0-$signi; $logei=$solui*$signi;
if($cntrsw<1){
$jline=1; while($jline<$nline){$jline++;
if($jline!=$iline){$vacuj=$vacus[$jline];
if($vacuj<1){$signj=$nands[$jline][$logei];
if($signj==$signi){$vacus[$jline]=1;};
if($signj==$signm){$nands[$jline][$logei]=0;
if($cardn[$jline]==1){print " CONTRADICTION!";
$cntrsw=1; $jline=$nline*$nline;
$iline=$nline*$nline;};};};};};};};};};
###
### RECALCULATE CARDINALITY.
if($cntrsw<1){$iline=1;
while($iline<$nline){$iline++; $vacui=$vacus[$iline]; $cardi=0;
if($vacui<1){$jname=1;
while($jname<$nname){$jname++; $signj=$nands[$iline][$jname];
if($signj!=0){$cardi++;};};}; $cardn[$iline]=$cardi;};
###
### RECALCULATE INITIAL SOLUTIONS.
$iline=1; while($iline<$nline){$iline++; $vacui=$vacus[$iline];
if($vacui<1){$cardi=$cardn[$iline];
if($cardi==1){$jname=1;
while($jname<$nname){$jname++; $signj=$nands[$iline][$jname];
if($signj!=0){$solui=$jname*$signj; $solun[$iline]=$solui;
if($signj==1){$plmn="-";}; if($signj==-1){$plmn="+";};
$nmslj=join('',$plmn,$name[$jname]); $slabl[$iline]=$nmslj;
print " $nmslj";};};};};};};};
###
### PRINT INPUT INSTRUCTIONS.
print qq|\n
To use the theorem prover, SELECT |;
print qq|\n and COPY a cascade hierarchy text-image from a |;
print qq|\n NOTEPAD® or other text-file; PASTE |;
print qq|\n the text image into the text box below; |;
print qq|\n and click on the SUBMIT button. |;
###
### INPUT POST METHOD.
print qq|\n
|;
###
### ADDITIONAL INSTRUCTIONS.
print qq|\n
The sentence parser is very fussy |;
print qq|\n and error-intolerant. The upper-left |;
print qq|\n corner must contain +a, one space |;
print qq|\n right of the left-margin. Each subsequent row |;
print qq|\n must contain exactly one variable name, preceded by |;
print qq|\n + or -, up to the final row. |;
print qq|\n Indentation must be EXACTLY THREE SPACES. |;
print qq|\n
For additional information, contact: |;
print qq|\n
|;
print qq|\n G. William Moore, MD, PhD. |;
###
### END JOB.
print qq|\n
Last modified: 2/17/2008, G. William Moore, MD, PhD. |;
print qq|\n
\n\n |; exit;
###
### Program modllive.cgi is a theorem-prover script, written
### in Perl, that serves as a companion to the manuscript:
### Moore GW, Brown LA, Burger RH, Hutchins GM, Miller RE.
### Modal Logic Theory for Pathology Inference. (Abstract).
### Arch Pathol Lab Med. 2004 Jun;128:.
### http://www.netautopsy.org/modlthry.htm
### http://apiii.upmc.edu/abstracts/posterarchive/2003/moore.html
###
### The input is a text-file, received from , which
### consists of an order logic hierarchy, as described in:
###
### Moore GW, Brown LA, Burger RH, Kao GF, Hutchins GM, Miller RE.
### Spreadsheet Order Logic for Pathology Inference. (Abstract).
### Arch Pathol Lab Med. 2005 Jun;129:.
### http://www.netautopsy.org/ordrlogc.htm
### http://apiii.upmc.edu/abstracts/display.cfm?id=262
###
### The ORIGIN of an order logic hierarchy is +0^ appearing
### in the firstline, one space right of the leftmost byte
### in the input file. All subsequent lines are indented
### in multiples of three spaces, as appropriate. Each line
### begins with + or - followed by the name of a single
### logical element (logel).
###
### There are three outcomes for a given input file:
### Theorem is vacuous.
### Theorem is inconsistent.
### Theorem has semantic content.
### A true theorem must always be vacuous....
###
### Every line in the datasource contains one logical element (=$logel).
### Every logel after $firstline=1 has exactly one parent.
### Terminal logels have no children.
### Every outcome is either vacuous, inconsistent, or has semantic content.
### A line is ACTIVE iff it has a child.
### A nandset is VACUOUS iff at least one logel is plus AND minus.
### A nandset is CONTRADICTORY iff has exactly one nonzero logel.
###
### $inputbox : primary data source, harvested from
### $outputbox : data source, after processing escape characters.
### $ndtbox : number of lines in datasource input box.
### $nline : number of lines in datasource.
### $iline, $jline, $kline : each line in datasource.
### $nname : number of named logic elements.
### $iname : each named logic element.
### $mxcol : maximum column number.
###
### $dtbox[$iline] : datasource input box, line-by-line.
### $dtsrc[$iline] : datasource, line-by-line.
### $logel[$iline] : logic element number for datasource line, $iline.
### $nmln[$iline] : logic element number for datasource line, $iline.
### $chlog[$iline] : logic element charstring for datasource line, $iline.
### $sign[$iline] : logic element sign for datasource line, $iline.
### $clmn[$iline] : column number for datasource line, $iline.
### $name[$iname] : name of logel variable $iname.
### $eman{$charstr}=$iname : $iname for char string $charstr.
### $fchld[$iline] : first child of line $iline; =0 if childless.
### $vacus[$iline] : =1 if line $iline is vacuous; =0 otherwise.
### $cardn[$iline] : cardinality for line $iline.
### $contr[$iline] : =1 if line $iline is contradictory; =0 otherwise.
### $solun[$iline] : solution for non-vacuous line $iline.
### $nands[$iline][$jline] : nandset at non-vacuous line $iline.
### $vacusw : =1 if every line is vacuous; =0 otherwise.
### $cntrsw : =1 if any line is contradictory; =0 otherwise.
###
###