checkmodal.perl:


#!/usr/local/bin/perl -w
# © Copyright 2001 by John Halleck, All rights reserved.

require 5.000;
use strict;
use Carp;

use vars qw(
   $printfile $line $lastline
   @expressions
   $count $item
   %have %forward %backward %full_fore %full_back %dualof
   %modalities $modality
   %left %right %equivalences %reductions
   $status
   %equiv_fore %equiv_back %equiv
   $duals $normal $beckersrule
   $intro $version
   $verbose
   %canned %canned_duals
   $INPUT %filechain
   %redundant
   %prefered
   %unnecessary
   %Operators
   $Had_Equivalences
   );

use FileHandle; # (So we can nest includes)

$version = "checkmodal version 0.64b 19 sep 2001\n"
         . "© Copyright 2001 by John Halleck, All Rights Reserved";

sub Introduction {
print <<INTRODUCTION
   This program takes in implications of the form of one modality implying
another (such as  Lp => p,   LLMp => MLLp, or ML <=> LM), it then does a very
quick analysis of the implications given. While the analysis is far from
complete, it might be useful, particularly in examining cases of adding
reductions to existing systems.
   The basic underlying assumptions that are being made here are that modus
tollens and double negation are availiable. And that strict implication is
transitive (And probably others that I've forgotten to mention.)

INTRODUCTION
;
   &help();
}

sub help {
print <<HELP
=help   # dumps at least this message.

One can get a summary of the system so far by putting in a line:
=summary             # for a complete summary of current status.
  =equivalences      # for a summary of just equivalence classes
  =implications      # for a summary of just current implications
  =crossreference    # for a summary of just current crossreferences

=save    Filename  # copy the inferences to a file.
=include Filename  # include contents of another file.

=duals   # Turns on processing of duals (the default)
         # (I.E., given  MLp => Lp, assume Mp => LMp)
=noduals # turns off processing of duals.

=beckersrule # Given xp => yp assume Lxp => Lyp; [Default]
=nobcckersrule # Don't assume Becker's rule.

=normal      # Assume this is a normal modal logic (Assumes, for example
             # that we have Becker's rule. [Default]
=nonormal    # don't assume it is normal (Containing the K axiom).

=fleshout    # Preform a simple brute force search for equivalence classes
             # based on the implications so far.
=hammerit    # An even more agressive search.

(The command line option   -n  turns off this tutorial.)

HELP
;
}


# ----------------------------------------------------------------------

# (I know I'm setting some of these to what they'd start out with
# anyway, but I may latter want reinitialization as a subroutine
# and this docuemnts the initial states.
@expressions = ();
$count = 0;         # Current line number.
%have = ();         # Which implications we actually have.
%dualof = ();       # The duals of various implications.
%modalities = ();   # Which modalities we've seen.
%left = ();         # The left hand side of an implication.
%right = ();        # The right hand side of an implication.
%forward = ();      # full set of forward implications from here.
%backward = ();     # full set of implications that imply this.
%equivalences = (); # Equivalence Classes.
%reductions = ();   #   A cannonical member of each class
%redundant = ();
%unnecessary = ();
%prefered     = (); # Prefered display form for this equivalence class.
$printfile = '';
%equiv_fore = ();   # Things this equivalence class implies.
%equiv_back = ();   # Things this equivalence class implied by.
%equiv = ();
$lastline = "=";
$duals = 1;
$intro = 1;
%equiv = ();
%full_fore = (); # Everything this equivalence class implies.
%full_back = (); # Everything that implies this equivalence class.
$verbose = 0;
$normal = 0;
$beckersrule = 1;
%filechain = ();
%redundant = ();

# ---------------------------------------------------------------------
# Canned lookups.
%canned = ();
$canned{'Lp => Mp'}  = "This is axiom D, characteristic of the system D";
$canned{'Lp => p'}   = "This is axiom T, characteristic of the system T";
$canned{'p => LMp'}  = "This is axiom B, characteristic of Brower systems.";
$canned{'Lp => LLp'} = "This is axiom 4, characteristic of S4 systems\n";
$canned{'Mp => LMp'} = "This is axiom 5, characteristic of S5 systems\n";
$canned{'Mp => p'}   = "*** Strange axiom for modal system ***";
$canned{'p => Lp'}   = "*** Strange axiom for modal system ***";
$canned{'Mp => Lp'}  = "*** Strange axiom for modal system ***";

%canned_duals = ();
$canned_duals{'p => Mp'}   = "This is the dual of axiom T.";
$canned_duals{'MLp => p'}  = "This is the dual of axiom B.";
$canned_duals{'MMp => Mp'} = "This is the dual of axiom 4.";
$canned_duals{'MLp => Lp'} = "This is the dual of axiom 5.";

# Canned operators:
$Operators{'=>'}   = '=>';
$Operators{'->'}   = '=>';
$Operators{'>'}    = '=>';
$Operators{'=='}   = '==';
$Operators{'='}    = '==';
$Operators{'<=>'}  = '==';
$Operators{'<==>'} = '==';
$Operators{'<->'}  = '==';
$Operators{'<'}    = '<=';
$Operators{'<-'}   = '<=';
$Operators{'<='}   = '<=';
# ---------------------------------------------------------------------

sub Dual { # Form the dual of a sequence of modals.
           # Given, for example  MMLMp  return LLMLp where the variable
           # is optional.
   my $expression = shift; confess ("No expression given in call to Dual")
                               if !defined $expression;
   my $result = '';
   $expression =~ s/M/Z/g; $expression =~ s/L/M/g; $expression =~ s/Z/L/g;
   return $expression;
}

# ---------------------------------------------------------------------

sub unique { # make a list with only unique elements.
   my @result = (); my $item;
   my %seen = ();
   foreach $item (@_) {
      if (!defined $seen{$item}) {
         $seen {$item} = 1;
         push @result, $item;
      }
   }
   return @result;
}

# ---------------------------------------------------------------------

sub modalsort {
  return @_ if @_ < 2;
  # print "DEBUG: modalsort got: @_\n";
  my @result = @_;
  if (@result == 0) { confess ("???  No data handed to modalsort???")};
  my $i; my $j;
  my $size = scalar (@_);
  # print "DEBUG: Size in modalsort was: $size\n";
  for ($i = 0; $i < $size-1; $i++) {
      confess ("??  no value in array??") if !defined $result[$i];
      confess ("??  Nil value in \$result[\$$i] ??") if '' eq $result[$i];
      my ($test1) =   $result[$i] =~ m/^([MLp]+)/;
      my $first  = length ($test1);
      for ($j = $i+1; $j < $size; $j++) {
          my ($test2) =  $result[$j] =~ m/^([MLp]+)/;
          my $second = length ($test2);
          if ($first > $second) {
             my $temp    = $result[$i];
             $result[$i] = $result[$j];
             $result[$j] = $temp;
             $first = $second;
             $test1 = $test2;
             # print "DEBUG: Swapped $result[$i] $result[$j], on length\n";
          } elsif ($first != $second) {
             # print "DEBUG: No swap on length $result[$i] $result[$j]\n";
             next;
          } elsif ($test1 gt $test2) {
             my $temp    = $result[$i];
             $result[$i] = $result[$j];
             $result[$j] = $temp;
             $first = $second;
             $test1 = $test2;
             # print "DEBUG: swap on value... $result[$i] $result[$j]\n";
          }
      }
      # print "DEBUG: After pass $i, @result\n";
  }
  # print "DEBUG: modalsort returning: @result\n";
  return @result;
}

# -----------------------------------------------------------------

# Turn a list of implications into a list of equivalence class implications.
sub equivimps {
   my $item; my @result=();
   foreach $item (@_) {
      push @result, $equivalences{$item};
   }
   return &modalsort (&unique (@result));
}

# -----------------------------------------------------------------
# find modalities matching a given one.

sub findmatches {
  my $base = shift; confess ("No base argument given to findmatches.")
                    if !defined $base;
  my $compare = shift; confess ("No compare argument given to findmatches")
                    if !defined $compare;
  my $prefix = '';  my $suffix = $compare;
  my @result = ();
  # print "DEBUG: findmatches ($base, $compare)\n";
  return ('', $compare) if $base eq '';
  return () if length($compare) < length($base);
  while (1) {
     last if (!$beckersrule) && ($prefix ne '');
     last if (!$normal) && ($prefix !~ m/^[L]*$/);
     # print "DEBUG: $prefix, $suffix,  base = $base, comp = $compare\n";
     if ($suffix =~ m/^$base(.*)$/) {
        push @result, $prefix, $1;
     }
     last if !$beckersrule; # Only substitution in that case.
     if ($suffix =~ m/^(.)(.*)$/) { $prefix .= $1; $suffix = $2 }
     else {last}
  }
  # print "DEBUG: findmatches returning ", join(", ", @result), "\n" if @result;
  return @result;
}

# -----------------------------------------------------------------
# match implications.

sub matchimplication {
   my $left = shift;
      confess ("No left argument given to matchimplication")
      if !defined $left;
   my $right = shift;
      confess ("No Right argument to matchimplication")
      if !defined $right;
   my $testleft = shift;
      confess ("No left test arguement to matchimplication")
      if !defined $testleft;
   my $testright = shift;
      confess ("No right test argument to matchimplication")
      if !defined $testright;
   return () if (length($left) > length($testleft)) ||
                (length($right) > length($testright));
   my @candidates = &findmatches ($left, $testleft);
   if (!@candidates) { return () }
   while (@candidates) {
      my $prefix = shift @candidates;
      my $suffix = shift @candidates;
         confess ("prefix $prefix didn't have matching suffix"
                 . " in matchimplication") if !defined $suffix;
      if (($prefix . $right . $suffix) eq $testright) {
          return ($prefix, $suffix);
      }
   }
   return ();
}

# -----------------------------------------------------------------
# Detect instances of other instances.

sub noteinstances {
   my $given = shift; confess "*** No equation given to noteinstances"
                      if !defined $given;
   # print "DEBUG: Noteinstances entered with $given\n";
   my $gotleft  = $left{$given}; confess "No left hand side to $given"
                                   if !defined $gotleft;
   my $gotright = $right{$given}; confess "No right hand side to $given"
                                   if !defined $gotright;
    $gotleft =~ s/p//; # Get raw modalities
    $gotright =~ s/p//;
   # print "DEBUG:      Raw pattern was \"$gotleft\"p => \"$gotright\"p\n";
   my $hadone = 0;
   foreach $item (&modalsort (keys %have)) {
      next if $item eq $given;
      # print "DEBUG:---  Checking given $given against earlier $item\n";
      my $leftitem = $left{$item};   $leftitem  =~ s/p//;
      my $rightitem = $right{$item}; $rightitem =~ s/p//;
      my ($prefix, $suffix) = &matchimplication ($gotleft, $gotright,
                                                 $leftitem, $rightitem);
      if (defined $suffix) {
         print "      Earlier $item is an instance of $given.\n";
         my $reason = '';
         $reason .= " (Becker's rule prefix \"$prefix\")"
             if $prefix ne '' and $beckersrule;
         $reason .=  "(Substituting ${suffix}p for p)" if $suffix ne '';
         print "        ", $reason, "\n";
         $redundant{$item} = "$given: $reason"
             if !defined $redundant{$item};
         $hadone = 1;
         last;
      }
    }
    # print "DEBUG:  ** Now checking reverse case\n";
    foreach $item (&modalsort (keys %have)) {
      next if $item eq $given;
      # print "DEBUG:---  Checking given $given against earlier $item\n";
      my $leftitem = $left{$item};   $leftitem  =~ s/p//;
      my $rightitem = $right{$item}; $rightitem =~ s/p//;
      my ($prefix, $suffix) = &matchimplication ( $leftitem, $rightitem,
                                                  $gotleft, $gotright);
      if (defined $suffix) {
         print "      $given is an instance of the earlier $item.\n";
         my $reason = '';
         $reason .= " (Becker's rule prefix $prefix)"
                                         if $prefix ne '' and ($normal
                                         or ($beckersrule and $prefix =~
                                                      m/^[L]+$/));
         $reason .=  " (Substituting ${suffix}p for p)"
             if $suffix ne '';
         print "        ", $reason, "\n";
         $redundant{$given} = "$item: $reason"
             if !defined $redundant{$given};
                   # ********************************************************************
         return 1; # ************ We don't need to be redundant multiple times **********
                   # ********************************************************************
      }
   }
   return $hadone;
}

# ---------------------------------------------------------------------
sub findchain {
   my $start = shift; confess "No starting modality given for findchain"
                          if !defined $start;
   my $goal  = shift; confess "No ending modality given for findchain"
                          if !defined $goal;
   my @exceptions = @_;
   my %except = ();
   my $item;
   foreach $item (@exceptions) { $except{$item} = 1 } # ignore these.
   my @todo = ($start);
   my %backchain = ();
   my %seen = ();
   while (@todo) {
      my $test = shift @todo;
      # print "DEBUG: Searching using $test (goal $goal)\n";
      if (defined $seen{$test}) { next }
      # print "DEBUG: We've not seen this modality on todo before.\n";
      $seen {$test} = 1;
      foreach $item (keys %have) {
         if (defined $except{$item}) { next } # things to ignore.
         # # print "DEBUG:    Testing \"$item\"\n";
         if ($left{$item} ne $test) {next}
         # print "DEBUG:    Testing \"$item\"\n";
         # print "DEBUG:       It has the correct left hand side.\n";
         my $rhs = $right {$item};
         if (defined $backchain{$rhs}) { next } # we can already get here.
         # print "DEBUG:       and it is a modality we haven't processed.\n";
         $backchain{$rhs} = $test;
         if ($rhs ne $goal) { push @todo, $rhs; next }
         # print "DEBUG:    *** Ok, we have the goal.\n";
         # print "DEBUG: backchain = ",
         #      join (", ", sort keys %backchain), "\n";
         # my $temp;
         # for $temp (sort keys %backchain) {
         #     print "DEBUG: $backchain{$temp} <= $temp\n";
         # }
         my @chain = ();
         while (defined $rhs) {
            # print "DEBUG: Accumulating $rhs in backchain\n";
            unshift @chain, $rhs;
            last if $rhs eq $start;
            # print "DEBUG:   And going for another:\n";
            $rhs = $backchain{$rhs};
            # print "DEBUG:   (which was $rhs)\n" if defined $rhs;
         }
         return @chain;
      } # end for each expression
   } # end while we have items to do.
   return ();
} # end findchain


sub displaychain { print join (' -> ', @_)}
sub stringchain {
  return join (' -> ', &findchain);
}

sub stringequiv {
   my $first = shift;  confess "No first argument to stringequiv\n"
                       if !defined $first;
   my $second = shift; confess "No second argument to stringequiv"
                       if !defined $second;
   my @oneway = &findchain ($first, $second);
   if (@oneway > 1) { pop @oneway }
   my @theother = &findchain ($second, $first);
   return join (' -> ', (@oneway, @theother));
}



sub Check_Degenerate {
   my $gotM = 0; my $gotL = 0, my $gotP = 0;
   foreach $item (@_) {
      if    ($item eq 'Mp') { $gotM = 1 }
      elsif ($item eq 'Lp') { $gotL = 1 }
      elsif ($item eq  'p') { $gotP = 1 }
   }
   if ($gotM && $gotL && $gotP) {
      warn "\n\n***\a This equivalence degenerates into the\n";
      warn "*** trival system (Where Mp == p == Lp).\n";
      warn '*** (' . &stringequiv ('Lp', 'Mp') . ")\n";
      warn  "***  Nothing further can be meaningfully added to this system.\n\n";
      return 2;
   } elsif ($gotL && $gotP) {
      warn "\n\n***\a This system just degenerated into the system\n";
      warn "*** where Lp == p", &stringequiv ('Lp', 'p'), "\n";
   } elsif ($gotM && $gotP) {
      warn "\n\n***\a This system just degenerated into the system\n";
      warn "*** where Mp == p", &stringequiv ('Mp', 'p'), "\n";
   } elsif ($gotM && $gotL) {
      warn "\n\n***\a The system now contains Mp == Lp.\n";
      warn '*** (' . &stringequiv ('Lp', 'Mp') . ")\n";
      warn "*** This system has become degenerate.\n\n";
   } else {
     return 0;
   }
   return 1;
}


sub make_equivalent {
   my $given  = shift;
   confess "No item in equivalence class passed to make_equivalent"
       if !defined $given;
   my @implications = keys %{$full_fore{$given}};
   my @total = ($given);
   my $item;
   foreach $item (@implications) {
      push @total, $item if defined ${$full_back{$given}}{$item};
   }
   if (@total < 2) {
      confess "No items in $given\'s equivalance class in make_equivalent";
   }
   @total = &modalsort (&unique (@total));
   # print "DEBUG: Total equivalence class to $given is @total\n";
   if (!@total) {
      confess "INTERNAL ERROR, making equivalence of singular modality.";
   } else {
      print "      Noting new equivalence class: ",
            join (" == ", @total), "\n";
      #print "DEBUG: Complete equivalence class is: @total\n";
      my @fore = (); my @aft = ();
      for $item (@total) {
          @fore = &unique ((@fore, @{$equiv_fore{$item}}));
          @aft  = &unique ((@aft,  @{$equiv_back{$item}}));
      }
      # print "DEBUG: Fore: @fore\n";
      # print "DEBUG:  Aft: @aft\n";
      my %seen = ();
      foreach $item (@total) { $seen{$item} = 1};
      @fore = grep {!$seen{$_}} @fore;
      @aft  = grep {!$seen{$_}} @aft;
      # print "DEBUG: Fore after cull: @fore\n";
      # print "DEBUG: Aft  after cull: @aft\n";
      my $smallist = length ($total[0]);
      my $equivtext = join ('/', grep {length($_) eq $smallist} @total);
      # print "DEBUG: equivtext is $equivtext\n";
      if (defined $prefered {$equivtext} )
         { # print "DEBUG: From $equivtext getting $prefered{$equivtext}\n";
           $equivtext = $prefered {$equivtext}
         } # We have a prefered form.
      elsif ($duals) { # We need to make a prefered form.
         my @duallist = (); my $current; my $final;
         foreach $current (@total) { push @duallist, &Dual($current) }
         @duallist = &modalsort (@duallist);
         my $realform = join ('/', grep {length($_) eq $smallist} @duallist);
         my $origform = &Dual($equivtext);
         $prefered {$origform} = $realform;
         # print "DEBUG: Preferred mapping = $origform => $realform\n";
         # print "DEBUG:    (Comming from $equivtext)\n";
      }
      my $reduced = $total[0]; # Remembering that total has been sorted.
                               # and is not empty.
      for $item (@total) {
          # print "DEBUG: Updateing equivalences for $item\n";
          $equivalences{$item} = $equivtext;
          $reductions{$item} = $reduced;
          @{$equiv{$item}} = @total;
      }
      @{$equiv_fore{$equivtext}} = @fore;
      @{$equiv_back{$equivtext}} = @aft;
      $Had_Equivalences = 1;
      return if 2 == &Check_Degenerate (@total);
      # print "DEBUG: Checking modalities for new equivalence classes. (Hoping for $reduced)\n";
      my $effective = 1; my $didsomething = 0;
      while ($effective) {
         $effective = 0;
         print "    Making an equivalence class reduction pass...\n" if $verbose;
         foreach $item (reverse &modalsort (keys %modalities)) {
           # print "DEBUG: Testing $item...\n";
           next if $item eq 'p';
           # print "DEBUG:       Not P\n";
           next if $item eq '';
           # print "DEBUG:       Not null\n";
           next if $item eq $reduced;
           # print "DEBUG:       Not equal to $reduced\n";
           next if $reductions{$item} eq $reduced;
           # print "DEBUG:       The reduction ($reductions{$item}) not equal to $reduced\n";
           my ($test, $reason) = &equivRreduction($item, '');
           next if $reason eq ''; # No reduction?
           &addmodality($test) if !defined $modalities{$test};
           # print "Testing $test($reductions{$test}) and $item($reductions{$item})\n" if $test ne $item;
           if ($reductions{$test} ne $reductions{$item}) {
              print "   Got one new equivalence...  $item<=>$test $reason\n";
              my $problem1 = &addimplication ($item, $test, "Equivalences $reason");
              my $problem2 = &addimplication ($test, $item, "Equivalences $reason");
              confess ("Internal error: New equivalence class without implicational impact?")
                 if $problem1 ne '' && $problem2 ne '';
              $effective = 1;    # We shouldn't be able to get here unless ONE of the two implications above
              $didsomething = 1; # was new.
           }
         }
      }
      # Bad idea: &fleshout() if $didsomething;
      # ??? Check degenerate?
   }
}


# --------------------------------------------------------------------------

sub cannon { # Cannonicalize a term
  my $expression = shift;
  confess ("No expression given in call to cannon") if !defined $expression;
  $expression =~ s/l/L/g;  $expression =~ s/m/M/g;
  if ($expression =~ m/[LM]$/) {$expression .= 'p' }
  return $expression;
}

# ------------------------------------------------------------------------

sub addmodality {
    my $given = shift; confess "No modality given to addmodality"
                           if !defined $given;
    if (defined $modalities{$given}) { return }
    $modalities {$given} = 1;
    $forward {$given} = []; # The modality implies noting yet.
    $backward{$given} = [];
    $equivalences {$given} = $given;
    $reductions   {$given} = $given;
    $equiv_fore{$given} = []; # And neither does it's (trivial)
    $equiv_back{$given} = []; # equivalence class.
    $full_fore{$given} = {};
    $full_back{$given} = {};
    $equiv{$given} = [$given];
}

# ------------------------------------------------------------------------

sub noteunnecessary {
  my $antecedent = shift; confess "No antecedent given to noteunnecessary"
                          if !defined $antecedent;
  my $consequent = shift; confess "No consequent given to noteunnecessary"
                          if !defined $consequent;
  my $reason = shift; confess "No reason given to noteunnecessary"
                          if !defined $reason;
  my $implication = $antecedent . ' => ' . $consequent;
  if (!defined $have {$implication}) {
    warn "***\a INTERNAL ERROR FOUND Attempt to mark non-existant implication\n";
    warn "***  \"$antecedent => $consequent\" as unnecessary. Please report this.\n";
    &summary();
    confess ("*** FATAL ERROR.");
  }
  $unnecessary {$implication} = $reason;
  $redundant   {$implication} = $reason;
  my $classleft = $equivalences{$antecedent};
}

# ------------------------------------------------------------------------

sub addimplication { # Add an implication to our tables.
   my $antecedent = shift; confess "No antecedent given to addimplication"
                               if !defined $antecedent;
   my $consequent = shift; confess "No consequent given to addimplication"
                               if !defined $consequent;
   my $reason = shift; confess "No reason given to addimplication"
                               if !defined $reason;
   my $silent = shift; $silent = 0 if !defined $silent;
   my $given   = $antecedent . ' => ' . $consequent;
   if (defined $have{$given}) {
      return "? We already have this implication.";
   }
   my $reduced = 0;
   my $test;
   $test = $reductions{$antecedent}; $test=$antecedent if !defined $test;
   if ($test ne $antecedent) {
      $reason .= " ($antecedent<->>$test)";
      $antecedent = $test; $reduced = 1;
   }
   $test = $reductions{$consequent}; $test=$consequent if !defined $test;
   if ($consequent ne $test) {
      $reason .= " ($consequent<->>$test)";
      $consequent = $test; $reduced = 1;
   }
   &addmodality ($antecedent) if !defined $modalities{$antecedent};
   &addmodality ($consequent) if !defined $modalities{$consequent};
   if ($equivalences{$antecedent} eq $equivalences{$consequent}) {
      return "? Both sides of this implication are in the same equivalence class";
   }
   if ($reduced) {
      my $new = $antecedent . ' => ' . $consequent;
      my $problem = "Prior equivalences reduce  $given  to  $new";
      $given = $new;
      if (defined $have{$given}) {
         $problem .=  "  (But we alreadly had that)";
         print "   ", $problem, "\n" if !$silent;
         return $problem;
      }
      if ($antecedent eq $consequent) {
         $problem .= "  But that gives no information...\n";
         print "   ", $problem, "\n" if !$silent;
         return $problem;
      }
      print "   ", $problem, "\n" if !$silent;
   }
   $left {$given} = $antecedent;
   $right{$given} = $consequent;
   if (defined ${full_fore{$antecedent}}{$consequent}) {
      print "   This implication already follows from the implications"
          . " already given.\n   " if !$silent;
      if (0 == &findchain ($antecedent, $consequent)) {
         warn "***\a INTERNAL CONSISTANCY ERROR IN PROGRAM\n";
         warn "*** WE THINK THERE IS AN IMPLICATION CHAIN BETWEEN\n";
         warn "*** $antecedent AND $consequent, BUT CAN'T FIND IT\n";
         warn "*** DUMPING INTERNAL TABLES:\n";
         &summary();
         confess "*** Please report this error.";
      }
      return "This line being ignored.";
   }
   $have {$given} = $reason;

   push @{$backward  {$consequent}}, $antecedent; # In now implies stuff,
   push @{$forward   {$antecedent}}, $consequent;
   push @{$equiv_fore{$equivalences{$consequent}}}, $antecedent;
      # and fix its equivalence
   push @{$equiv_back{$equivalences{$antecedent}}}, $consequent; # class

   ${$full_fore{$antecedent}}{$consequent} = 1; # Accumulate all implications
   ${$full_back{$consequent}}{$antecedent} = 1;

   # print "DEBUG: full back of $antecedent = ",
   #       join (", ", keys %{$full_back{$antecedent}}), "\n";
   # print "DEBUG: full back of $consequent = ",
   #       join (", ", keys %{$full_back{$consequent}}), "\n";
   # print "DEBUG: full fore of $antecedent = ",
   #       join (", ", keys %{$full_fore{$antecedent}}), "\n";
   # print "DEBUG: full fore of $consequent = ",
   #       join (", ", keys %{$full_fore{$consequent}}), "\n";

   my @forelist = keys %{$full_fore{$consequent}};
   my @backlist = keys %{$full_back{$antecedent}};

   # print "DEBUG: filling in back items:\n";
   my $temp; my $item;
   foreach $item (@backlist) {
      foreach $temp (@forelist, $consequent) {
        next if $temp eq $item;
        # print "DEBUG: adding $temp to fore list of $item\n"
        #    if !defined ${$full_fore{$item}}{$temp};
        ${$full_fore{$item}}{$temp} = 1;
        # print "DEBUG: adding $item to back list of $temp\n"
        #    if !defined ${$full_back{$temp}}{$item};
        ${$full_back{$temp}}{$item} = 1;
      }
   }
   # print "DEBUG: filling in forward items\n";
   foreach $item (@forelist) {
      foreach $temp (@backlist, $antecedent) {
         next if $temp eq $item;
         # print "DEBUG: adding $temp to back list of $item\n"
         #    if !defined ${$full_back{$item}}{$temp};
         ${$full_back{$item}}{$temp} = 1;
         # print "DEBUG: adding $item to fore list of $temp\n"
         #    if !defined ${$full_fore{$temp}}{$item};
         ${$full_fore{$temp}}{$item} = 1;
      }
   }

   # print "DEBUG: AFTER recurrance, we have:\n";
   # print "DEBUG:   full back of $antecedent = ",
   #       join (", ", keys %{$full_back{$antecedent}}), "\n";
   # print "DEBUG:   full back of $consequent = ",
   #       join (", ", keys %{$full_back{$consequent}}), "\n";
   # print "DEBUG:   full fore of $antecedent = ",
   #       join (", ", keys %{$full_fore{$antecedent}}), "\n";
   # print "DEBUG:   full fore of $consequent = ",
   #       join (", ", keys %{$full_fore{$consequent}}), "\n";

   if ((defined ${full_fore{$consequent}}{$antecedent})
   and (defined ${full_fore{$antecedent}}{$consequent})) {
      #print "DEBUG: we've gotten an equivalence relation from this "
      #    . "implication\n";
      &make_equivalent($consequent, $antecedent);
      return '';
   }

   # OK, we know that this is not part of an equivalence class.

   # Has this made anything else redundant (Not meaningfull if equivalence)?
   foreach $item (keys %{$full_back{$antecedent}}) {
      if (defined $have{"$item => $consequent"}) {
         my @temp = &findchain($item, $consequent, "$item => $consequent");
         if (@temp) {
            print "   This implication makes the previous implication:"
                . " $item => $consequent\n";
            print "   redundant. (Its function still exists in the inference "
                . "chain:\n      ";
            &displaychain(@temp);
            print ")\n";
            &noteunnecessary ($item, $consequent, join (' -> ', @temp));
        }
      }
   }
   foreach $item (keys %{$full_fore{$consequent}}) {
      if (defined $have{"$antecedent => $item"}) {
         my @temp = &findchain($item, $consequent, "$item => $consequent");
         if (@temp) {
            print "   This implication makes the previous implication:\n";
            print "      $item => $consequent\n";
            print "   redundant. (Its function still exists in the inference "
                . "chain:\n      ";
            &displaychain(@temp);
            print ")\n";
            &noteunnecessary ($item, $consequent, join (' -> ', @temp));
         }
      }
   }

   return '';
}


# ----------------------------------------------------------------------

sub makedual {
  my $left = shift; confess ("No antecedent in makedual")
                    if !defined $left;
  my $right = shift; confess ("No consequent in makedual")
                    if !defined $right;
  my $implication = $left . ' => ' . $right;
  my $left_dual = &Dual ($left);
  my $right_dual = &Dual ($right);
  my $impdual = $right_dual . ' => ' . $left_dual;
  $dualof{$implication} = $impdual;
  $dualof{$impdual}     = $implication;
  return ($right_dual, $left_dual, $impdual);
}

# ----------------------------------------------------------------------

sub addpair {
  my $antecedent   = shift; confess ("No antecedent in add_pair")
                            if !defined $antecedent;
   my $consequent  = shift; confess ("No consequent in add_pair")
                            if !defined $consequent;
   my $reason = shift; confess ("No reason given in addpair")
                            if !defined $reason;
   my $implication = $antecedent . ' => ' . $consequent;
   print '   Adding: ', $implication, ' (', $reason, ")";
   print ' ', $canned{$implication}
      if defined $canned{$implication};
   print ' ', $canned_duals{$implication}
      if $duals && defined $canned_duals{$implication};
   print "\n";
   my $problems = &addimplication ($antecedent, $consequent, $reason);
   print '      ', $problems, "\n" if $problems ne '';
   if ($duals){  # Only add duals if asked to.
      my ($newleft, $newright, $full_dual) =
         &makedual($antecedent, $consequent);
      if ($full_dual eq $implication) {
         print "   [This implication is self dual]\n";
      } elsif (!defined $have{$full_dual}
       && !defined ${$full_fore{$newleft}}{$newright} ) {
         print "      Adding dual: $full_dual\n";
         $problems = &addimplication ($newleft, $newright, "Dual of $implication");
         print '      ', $problems, "\n" if $problems ne '';
         $redundant{$full_dual} = "Dual of $implication";
      }
   }
   print "\n";
   return;
}

# ----------------------------------------------------------------------

sub processrawpair {
  my $antecedent = shift; confess ("No antecedent in processrawpair")
                           if !defined $antecedent;
  my $consequent = shift; confess ("No consequent in processrawpair")
                           if !defined $consequent;
  my $reason = shift; confess ("No reason in processrawpair")
                           if !defined $reason;
  my $implication = $antecedent . ' => ' . $consequent;
  if ((!defined $modalities{$antecedent}) ||
      (!defined $modalities{$consequent}) ||
      ((!defined $have{$implication}) &&
         !defined ${$full_fore{$antecedent}}{$consequent})) {
      &addpair ($antecedent, $consequent, $reason);
      $redundant{$implication} = $reason;
      return $implication;
  }
  return '';
}

# ---------------------------------------------------------------------

sub processitem {
  my $antecedent = shift; confess ("No antecedent in processitem")
                           if !defined $antecedent;
  my $consequent = shift; confess ("No consequent in processitem")
                           if !defined $consequent;
  my $reason = shift; confess ("No reason in processitem")
                           if !defined $reason;
  my $implication = $antecedent . ' => ' . $consequent;
  if ((!defined $modalities{$antecedent}) ||
      (!defined $modalities{$consequent}) ||
      ((!defined $have{$implication}) &&
         !defined ${$full_fore{$antecedent}}{$consequent})) {
      print "   Adding: $implication,  ($reason)\n";
      &addimplication ($antecedent, $consequent, $reason);
      # ??? No error checking here?
      $redundant{$implication} = $reason if !defined $redundant{$implication};
      return $implication;
  }
  return '';
}

# ----------------------------------------------------------------------

sub processset {
  my $antecedent = shift; confess ("No antecedent in processset")
                           if !defined $antecedent;
  my $consequent = shift; confess ("No consequent in processset")
                           if !defined $consequent;
  my $reason = shift; confess ("No reason in processset")
                           if !defined $reason;
  my $implication = $antecedent . ' => ' . $consequent;
  # print "DEBUG: Processing set: $antecedent => $consequent\n";
  &processitem ($antecedent, $consequent, $reason);
  $antecedent =~ s/p//; $consequent =~ s/p//;
  &processitem ($antecedent . 'Lp', $consequent . 'Lp',
                $implication . ', p/Lp');
  &processitem ($antecedent . 'Mp', $consequent . 'Mp',
                $implication . ', p/Mp');
  return if !$duals;
  my $left = &Dual($consequent); my $right = &Dual($antecedent);
  my $dual = "${left}p => ${right}p";
  &processitem ($left .  'p', $right .  'p', 'Dual of ' . $implication);
  &processitem ($left . 'Lp', $right . 'Lp', "$dual, p/Lp");
  &processitem ($left . 'Mp', $right . 'Mp', "$dual, p/Mp");
}

# ----------------------------------------------------------------------

sub expanditem {
   my $left = shift; confess ("No antecedent in expanditem")
                           if !defined $left;
   my $right = shift; confess ("No consequent in expanditem")
                           if !defined $right;
   my $reason = shift; confess ("No reason given in expanditem")
                           if !defined $reason;
   my $implication = $left . ' => ' . $right;
   # print "DEBUG: Expanding item $left => $right\n";
   &processset ($left, $right, $reason);
   if ($beckersrule) {
      &processset ('L' . $left, 'L' . $right, "$implication, Becker's rule [L]");
      &processset ('M' . $left, 'M' . $right, "$implication, Becker's rule [M]");
   }
}

# ---------------------------------------------------------------------

sub equivRreduction {
  my $test = shift;
     confess "No modality handed to equivRreduction" if !defined $test;
  my $given = $test;
  my $reason = shift;
     confess "No reason handed to equivRreduction" if !defined $reason;
  my $peeled = '';
  while ($test =~ m/^(.*)(L|M)p$/) {
     $peeled = $2 . $peeled;
     my $try = $1 . 'p';
     # print "DEBUG:   Trying $try, peeled = '$peeled'\n";
     if ((defined $reductions{$try}) && $reductions{$try} ne $try) {
        my $oldtry = $try; $oldtry =~ s/p$//;
        $try = $reductions{$try}; $try =~ s/p$//;
        my $reasontry = "[$try]${peeled}p";
        $try .= $peeled . 'p';
        my $reasonold = "[$oldtry]${peeled}p";
        $reason .= "($reasonold<=>$reasontry)";
        # print "DEBUG:      Reduces $given <=> $try\n";
        return &equivRreduction($try, $reason);
     }
     $test = $try;
  }
  # print "DEBUG:     Nothing... just returning original\n";
  return ($given, $reason);
}

# ----------------------------------------------------------------------

sub process_full_pair {
   my $antecedent = shift; confess ("No antecedent in process_full_pair")
                           if !defined $antecedent;
   my $consequent = shift; confess ("No consequent in process_full_pair")
                           if !defined $consequent;
   my $reason = shift; confess ("No reason given in process_full_pair")
                           if !defined $reason;
   $antecedent = &cannon($antecedent);
   $consequent = &cannon($consequent);
   if ($antecedent eq $consequent) {
      print "   This is the trivial implication\n";
      return;
   }
   if ($antecedent eq $consequent) {
      print "   this is the trivial implication.\n";
      return;
   }
   &addmodality($antecedent) if !defined $modalities{$antecedent};
   &addmodality($consequent) if !defined $modalities{$consequent};
   if ($reductions{$antecedent} eq $reductions{$consequent}) {
      print "   But both sides are in the same equivalence class already.\n";
      return;
   }
   # my $antecedentdual = &Dual ($antecedent) if $duals;
   # my $consequentdual = &Dual ($consequent) if $duals;
   # my $rawantecedent = $antecedent; $rawantecedent =~ s/p//;
   # my $rawconsequent = $consequent; $rawconsequent =~ s/p//;
   # my $rawdualantecedent = $antecedentdual; $rawdualantecedent =~ s/p//;
   # my $rawdualconsequent = $consequentdual; $rawdualconsequent =~ s/p//;
   my $implication = "$antecedent => $consequent";
   my $text;
#  # The assumption here must be that it's already been printed.
   if ($have{$antecedent . '=>' . $consequent}) {
      print "    We already have this implication.\n";
      return;
   }
   if (defined ($text = $canned{$implication})) {
      print "      ", $text, "\n";
   }
   if ($duals && defined ($text = $canned_duals{"$antecedent => $consequent"})) {
      print "      ", $text, "\n";
      print "      And deductivly equivalent to it\n" if $duals;
   }
   &addpair ($antecedent, $consequent, $reason);
   my $needspace = &noteinstances ($implication);
   $needspace |= &noteinstances ($dualof{$implication}) if $duals;
   print "\n" if $needspace;
   # In the absense of substituition or Becker's rule, we'd be done.
   # But we always have at least substitution.
   &expanditem ($antecedent, $consequent, $reason);
}

# ----------------------------------------------------------------------

sub fleshout {
  my $level = shift; $level = 0 if !defined $level;
  # print "Debug: Entering fleshout.\n";
  my $equation;
  foreach $equation (&modalsort(keys %have)) {
     # print "DEBUG: hashing out $equation\n";
     my $antecedent = $left{$equation};  my $consequent = $right{$equation};
     my $left  = $antecedent;
     my $right = $consequent;
     next if (length($left) < length($right)) && $level == 0;
     # print "DEBUG: might be a reduction...\n";
     next if defined $equivalences{$left}  &&
             defined $equivalences{$right} &&
             $equivalences{$left} eq $equivalences{$right};
     # print "DEBUG: reduction not in the same equivalence class. $left => $right\n";
     &expanditem ($left, $right, '???');
     $left =~ s/p//; $right =~ s/p//;
     my $item;
     foreach $item (&modalsort (keys %modalities)) {
        next if $item eq $antecedent;
        # print "DEBUG:    Checking $item for implicational possibilities.\n";
        my $original = $item;
        $item =~ s/p//;
        my @candidates = &findmatches ($left, $item);
        next if !@candidates; # if we don't have a match, punt.
        # print "DEBUG: Possibilities for $left => ${item}p: \"",
        #      join ("\", \"", @candidates), "\"\n";
        my @tests = ();
        my @reasons = ();
        while (@candidates) {
           my $suffix = pop @candidates;
           my $prefix = pop @candidates;
           # print "DEBUG: Match was with \"$prefix\" \"$suffix\"\n";
           push @tests, $prefix . $right . $suffix . 'p';
           my $reason = "$antecedent => ${right}p,";
           $reason .=  " Becker's prefix $prefix" if $prefix ne '';
           $reason .= ',' if $prefix ne '' && $suffix ne '';
           $reason .=  " p/${suffix}p" if $suffix ne '';
           push @reasons, $reason;
           # print "DEBUG:    considering \"$prefix\" \"$right\" \"$suffix\" p\n";
        }
        @tests = &unique (@tests);
        # print "DEBUG: possible right hand sides are: ", join (", ", @tests), "\n";
        my $reason;
        my $possibility;
        foreach $possibility (@tests) {
           $reason = pop @reasons;
           next if $item eq $possibility;
           my $implication = $item . 'p => ' . $possibility;
           # print "DEBUG: We already have $implication\n" if defined $have{$implication};
           next if defined $have{$implication};
           if (defined $full_fore{$original} and
               !defined ${$full_fore{$original}}{$possibility}) {
              # print "DEBUG: *** trying $implication\n";
              &addpair ($original, $possibility, $reason);
              $redundant{$implication} = $have {$implication};
           } else {
              # print "DEBUG: We already have the functionaltity of $implication\n";
           }
        }
     }
   }
}

# ----------------------------------------------------------------------

sub listequivtb {
   print "\n\nRaw equivalences table.\n";
   my $item;
   foreach $item (&modalsort (keys %equiv)) {
      print "@{$equiv{$item}}\n"
   }
}


sub listreachability {
   print "\n\nModality reachabilities:\n";
   my $item;
   foreach $item (&modalsort (keys %modalities)) {
      my @to   = &modalsort (keys %{$full_fore{$item}});
      my @from = &modalsort (keys %{$full_back{$item}});
      print "$item (<= @from) (=> @to)\n";
   }
}


sub makeprintlist {
   my $text = shift; confess ("No text argument given to makeprintlist")
                     if !defined $text;
   my @given = @_;
   return '' if @given == 0;
   return $text . ' ' . join (', ', @given);
}

sub expandto {
   my $text = shift; confess ("expandto given no text") if !defined $text;
   my $size = shift; confess ("expandto given no size") if !defined $size;
   while (length($text) < $size) { $text .= ' ' }
   return $text;
}

sub maxsize {
   my $size = 0;
   my $item;
   return 0 if 0 == @_;
   foreach $item (@_) {
      $size = length ($item) if length($item) > $size;
   }
   return $size;
}

sub dumplists {
   confess ("dumplists given no arguments") if @_ < 1;
   my @given = @_; my $last = pop @given;
   my @sizes = (); my $item;
   foreach $item (@given) {
      push @sizes, &maxsize (@$item);
   }
   while (scalar (@$last) > 0) {
     my $i;
     for ($i = 0; $i < @given; $i++) {
         my $array = $given[$i];
         print &expandto (shift @$array, $sizes[$i]), '  ';
     }
     print shift @$last, "\n";
   }
}


sub listcrossreferences {
   my $item;
   my @first = (); my @second = ();  my @third = ();
   print "\n\nCross References:\n";
   foreach $item (&modalsort (keys %modalities)) {
     push @first, $item;
     push @second, &makeprintlist ("implied by",
                                   &modalsort (@{$backward{$item}}));
     push @third,  &makeprintlist ("it implies",
                                   &modalsort (@{$forward {$item}}));
   }
   &dumplists (\@first, \@second, \@third);
}


sub listnonredundant {
    my $item; my $implies;
    my @from = (); my @op = (); my @into = ();
    my %done = ();
    print "\n\nNon-redundant implications.\n";
    foreach $item (&modalsort (keys %have)) {
         if ($have{$item} =~ m/^Given/ && !defined $redundant{$item}) {
            push @from, $left{$item};
            push @op, '=>';
            push @into, $right{$item};
            next if !$duals;
            my $thedual = $dualof{$item};
            next if !defined $thedual;
            next if $item eq $thedual;
            $done{$thedual} = 1; # Since it is the dual of one we've done.
         }
    }
    &dumplists (\@from, \@op, \@into);
    print "---";
}


sub cleanequivalences {
  my $temp = shift; confess ("No argument handed to cleanequivalences")
                    if !defined $temp;
  my $towards = &makeprintlist ('implied by',
                                 &equivimps  (@{$equiv_fore{$temp}}));
  my $away    = &makeprintlist ('it implies',
                                 &equivimps  (@{$equiv_back{$temp}}));
  if ($temp !~ m/^M/) {
     return ($temp, $towards, $away);
  } else {
     return ($temp, $away, $towards);
  }
}

sub dualexpression {
  my $given = shift; confess ("No argument handed to dualexpression")
                     if !defined $given;
  my $direction = '';
  if ($given =~ m/^it implies (.*)$/) {
      $direction = 'implied by '; $given = $1;
  } elsif ($given =~ m/^implied by (.*)$/) {
      $direction = 'it implies '; $given = $1;
  }
  my @list = split (', ', $given);
  my @result = ();
  my $item;
  foreach $item (@list) {
     $item = &Dual($item);
     $item = $prefered{$item} if defined $prefered{$item};
     push @result, $item;
  }
  return $direction . join (', ', @result);
}

sub listequivalences {
   print "\n\nEquivalence Classes so far:\n";
   my %done = ();
   my $item;
   my @first = (); my @second = (); my @third = ();
   foreach $item (&modalsort (values %equivalences)) {
      next if defined $done{$item};
      $done {$item} = 1;
      my ($name, $anti, $cons) = &cleanequivalences($item);
      push @first, $name; push @second, $anti; push @third, $cons;
      next if !$duals;
      # print "DEBUG: Just did $name\n";
      my $namedual = &dualexpression ($name);
      # print "DEBUG:   dual was $namedual\n";
      if (defined $prefered{$namedual}) { $namedual = $prefered{$namedual} }
      # print "DEBUG:   after preferences it was: $namedual\n";
      if ($namedual ne $name and !defined $done{$namedual}) {
         next if defined $done{$namedual};
         $done{$namedual} = 1;
         push @first, $namedual;
         push @second, &dualexpression ($anti);
         push @third,  &dualexpression ($cons);
      }
      push @first, ''; push @second, ''; push @third, '';
   }
   &dumplists (\@first, \@second, \@third);
   print "---";
}


sub listimplications {
   my $item; my $implication; my $thisone;
   my @from = (''); my @op = (''); my @into = ('');
   my @source = ('source'); my @status = ('Redundancies');
   print "\n\nImplications.\n";
   foreach $item (&modalsort (keys %modalities)) {
     next if 0 == @{$forward{$item}};
     foreach $implication (&modalsort (@{$forward{$item}})) {
           $thisone = "$item => $implication";
           push @from, $item;
           push @op, '=>';
           push @into, $implication;
           my $kind   = $redundant{$thisone}; $kind   = '' if !defined $kind;
           my $origin = $have{$thisone};      $origin = '' if !defined $origin;
           $kind = '' if $origin eq $kind;
           push @source, $origin;
           push @status, $kind;
     }
   }
   &dumplists (\@from, \@op, \@into, \@source, \@status);
   print "---";

}



sub summary {
   &listimplications();
   &listcrossreferences();
   &listnonredundant();
   &listequivalences();
}

sub processfile {
  my $thisfile = shift;  confess "No file handed to processfile\n"
                       if !defined $printfile;
  my $oldcount = $count;
  my $oldinput = $INPUT;
  my $oldprint = $printfile;
  $INPUT = new FileHandle;
  $count = 0;
  if (defined $filechain{$thisfile}) {
     warn "*** Circular file include chain...\n";
     warn "*** " . join (", ", &modalsort (keys %filechain)) . ', '
        .  $thisfile . "\n";
     die  "*** Executation terminated.\n";
  } else {
     $filechain{$thisfile} = 1
  }
  if    ((-e $thisfile          ) and open ($INPUT, $thisfile))         {}
  elsif ((-e $thisfile . '.data') and open ($INPUT, $thisfile.'.data')) {}
  elsif ((-e $thisfile . '.txt' ) and open ($INPUT, $thisfile.'.txt'))  {}
  elsif ((-e $thisfile . '.text') and open ($INPUT, $thisfile.'.text')) {}
  elsif ((-e "/home/nahaj/includes/logic-systems/$thisfile.data")
       and open ($INPUT, "/home/nahaj/includes/logic-systems/$thisfile.data"))
                                                                        {}
  else {
     warn ("\n\n***\a Unable to open file \"$thisfile\" ($!)\n");
     next;
  }
  if ($printfile ne '') {
      $printfile = $oldprint . '(' . $oldcount . '):' . $thisfile;
  } else {
      $printfile .= $thisfile;
  }
  while (defined ($line = <$INPUT>)) { &processinput($line); print "\n" }
  if (!close ($INPUT)) {
     warn "Unable to close $thisfile ($!) \n";
     # print "DEBUG: (chain includes: ", join (", ", keys %filechain), "\n";
  }
  undef $filechain{$thisfile};
  $count     = $oldcount;
  $INPUT     = $oldinput;
  $printfile = $oldprint;
}

# ------------  PROCESS INPUT ---------------------------------

sub processinput {
  my $line = shift; return if !defined $line;
  chomp $line; $lastline = $line;
  $count++;
  if ($printfile ne '') {print "$printfile($count): ", $line, "\n" }
  else                  {print            "$count: ",  $line, "\n" }
  if ($line =~ m/^([^\#]*)\#/) { $line = $1 }
  $line =~ s/\s+$//g; $line =~ s/^\s+//g; $line =~ s/\s\s/ /g;
  return if $line eq '';
  if ($line =~ m/^=\s*(.+)$/) { # command?
     $line = lc $1;
     if    ($line eq "summary")         { &summary             () }
     elsif ($line eq "help")            { &help                () }
     elsif ($line eq "equivalences")    { &listequivalences    () }
     elsif ($line eq "implications")    { &listimplications    () }
     elsif ($line eq "crossreferences") { &listcrossreferences () }
     elsif ($line eq "eq")              { &listequivtb         () }
     elsif ($line eq "nonredundant")    { &listnonredundant    () }
     elsif ($line eq "duals") {
        $duals = 1;
        print "    For Ap => Bp, we can also generate Dual(B)p => Dual(A)p\n";
        }
     elsif ($line eq "noduals"){
        $duals = 0;
        print "    Only the implications specificly given will be entered.\n";
        print "    (No attempt will be made to use duals)\n";
        }
     elsif ($line eq "beckersrule") {
        $beckersrule = 1;
        print "    From xp => yp we can assume Lxp => Lyp\n";
        }
     elsif ($line eq "nobeckersrule") {
        $beckersrule = 0;
        print "    No Becker's rule implications will be assumed.\n";
        }
     elsif ($line eq 'normal') {
        print "    System will be assume to be a normal (K) system.\n";
        print "    (With necessitation, and Becker's rule.)\n";
        print "    We will assume  xp => yp  also means that we can assume\n";
        print "    both  Mxp => Myp  and  Lxp => Lyp\n";
        $normal = 1;
        }
     elsif ($line eq "fleshout") {
        &fleshout(0);
        }
     elsif ($line eq "hammerit") {
        &fleshout(1)
        }
     elsif ($line eq "nonormal") {
        print "    We assume that the system is not a normal (K) system\n";
        $normal = 0;
        }
     elsif ($line =~ m/^save(.+)$/) {
        my $file = $1;
        if ($file =~ m/^[^\.]+$/) { $file .= '.data' }
        if (-e $file) {
           print "*** Sorry, but that file already exists.\n";
           return;
        } elsif (!open (TEMP, ">$file")) {
           print "Unable to open the file \"$file\" for saving. $!\n";
        } else {
           my $remaining;
           if ($duals)       { print TEMP "=duals\n" }
           else              { print TEMP "=noduals\n" }
           if ($normal)      { print TEMP "=normal\n" }
           else              { print TEMP "=nonormal\n" }
           if ($beckersrule) { print TEMP "=beckersrule\n" }
           else              { print TEMP "=nobeckersrule\n" }
           my %done = ();
           foreach $remaining (&modalsort (keys %have)) {
              next if defined $done{$remaining};
              print TEMP $remaining, "\n";
              $done{$remaining} = 1;
              next if !$duals;
              my $temp = $dualof{$remaining};
              die "No duals when \$duals set? $remaining\n" if !defined $temp;
              $done{$temp} = 1;
           }
           close (TEMP) or print "Couldn't close Save file. $!\n";
        }
        print "Ok, we've saved the state to the file \"$file\"\n";
        }
     elsif ($line =~ m/^include\s+(.+)$/) {
           my $file = $1;
           &processfile ($file);
        }
     elsif ($line eq "reachability") { &listreachability() }
     elsif ($line eq 'exit' || $line eq 'quit') {
        die "Done.\n";
        }
     else {
        print "??? Bad command \"$line\"\n";
     }
     return;
  } elsif ($line =~ m/^\!(.*)$/) {
     my $wegot = $1;
     warn ("??? No unix shell escapes allowed.\n");
     warn ("?????? Not even for the infamous vi editor.\n") if $wegot eq 'vi';
     warn ("?????? Not even for the EMACS editor\n")        if $wegot eq 'emacs';
     warn ("?????? Not even for the pine mailer\n")         if $wegot eq 'pine';
     warn ("?????? What previous command?\n")               if $wegot eq '!';
     warn ("?????? And definitely not with editing.\n")     if $wegot =~ m;^/; ;
     return;
  } elsif ($line =~ m/^(\w+)$/) {
     if ($1 eq 'exit' or $1 eq 'quit' or $1 eq 'stop') {
        warn ("EXITING PROGRAM\n");
        &summary();
     } elsif ($1 eq 'pine') { warn "??? Programs can't pine for anyone.\n" }
       elsif ($1 eq 'vi')   { warn "??? Vi the light, of the silvery moon.\n"}
       elsif ($1 eq 'emacs'){ warn "??? I like E Mac's also. (and I-MACS's)\n"}
       elsif ($1 eq 'ls')   { warn "??? 'ls' is not 'sl'\n"}
       elsif ($1 eq 'sl')   { warn "??? sl-iver slippers...\n"}
       else                 { warn ("???  Unprocessable line: $1\n") }
     return;
  }
  $line =~ s/\s//g;
  if ( $line !~ m/^(\w+)(=>|->|>|==|=|<->|<=>|<==>|<=|<-|<)(\w+)$/ ) {
     warn ("??? Malformed line: $printfile:$count:  $lastline\n");
     return;
  }
  my ($lhs, $op, $rhs) = ($1, $2, $3);
  my $cannonicalop;
  if (!defined ($cannonicalop = $Operators{$op})) {
     print "  Unknown operator \"$op\"\n";
     print "  This line being ignored.\n";
     return;
  }
  if ($cannonicalop eq '<=') {
     my $temp = $rhs; $rhs = $lhs; $lhs = $temp;
     $cannonicalop = '=>';
  }
  $op = $cannonicalop;
  $lhs = &cannon($lhs); $rhs = &cannon($rhs);
  if ($lhs eq $rhs) {
     print "   This doesn't change the sytem (since both sides are the same)\n";
     print "   so we'll ignore it.\n";
     return;
  } elsif ((defined $equivalences{$lhs}) && (defined $equivalences{$rhs})
          && $equivalences{$lhs} eq $equivalences{$rhs}) {
     print "   This relates two modalities already in the same" .
           " equivalence class\n   ($equivalences{$lhs})\n";
     print "   *** This line being ignored.\n";
     return;
  } elsif ($op eq '==') {
     # what to check?  (We already know they aren't the same equivalence
     #                  class, so one implication must not be here...)
     if (defined $have{$lhs . ' => ' . $rhs}) {
        $op = '=>';
        my $temps = $lhs; $lhs = $rhs; $rhs = $temps;
     } elsif (defined $have{$rhs . ' => ' . $lhs}) {
        $op = '=>';
     }
  }
  if (defined $have{$lhs . ' => ' . $rhs}) {
     print "   This is an implication that is already in the tables.\n";
     print "   *** This line was ignored.\n";
     return;
  }
  if (defined ${$full_fore{$lhs}}{$rhs}) {
     print "   This implication is already implied by preceeding implications.\n";
     print "   ("; &displaychain(&findchain ($lhs, $rhs)); print ")\n";
     print "   *** This line was ignored.\n";
     return;
  }
  my $reason;
  if ($printfile ne '') {
     $reason = 'Given, file ' . $printfile . '#' . $count;
  } else {
     $reason = 'Given, line ' . $count;
  }
  $Had_Equivalences = 0;
  if ($op eq '=>' || $op eq '==') {
     &process_full_pair ($lhs, $rhs, $reason);
  }
  if ($op eq '==') {
     &process_full_pair ($rhs, $lhs, $reason);
  }
  &fleshout() if $Had_Equivalences;
  $Had_Equivalences = 0;
} # End processing input



# =====================  MAIN LOOP ============================



print $version, "\n\n";


# Handle command line options.
my @files = ();
while (@ARGV) {
   $item = shift @ARGV;
   if ($item !~ m/^\-/) {
      push @files, $item;
   }elsif ($item !~ m/^\-(\w*)$/) {
      die ("\n\n*** Malformed command line option: $1\n");
   } elsif (lc ($1) eq 'n') {
      $intro = 0;
   } elsif ($1 eq '?' or lc ($1) eq 'help') {
      print "\nAvailiable command line options are:\n";
      print "  -n  don't print the introduction message.\n";
      print "  -v  Verbose mode.\n";
      print "\n";
   } elsif (lc ($1) eq 'v') {
      $verbose = 1;
   } else {
     die "\n\n*** Unknown command line option: $1\n";
   }
}

&Introduction() if $intro;


my $givenfile;
foreach $givenfile (@files) {
  $count = 0;
  &processfile ($givenfile);
}

$count = 0;
$printfile = '';
print "\n\nInput an implication or a command: ";
while (defined ($line = <>)) {
   chomp $line;
   &processinput ($line);
   print "\nInput ", $count+1, ": ";
}

&summary if $lastline !~ m/^\s*\=/;

print "\nDone.\n";

exit 0;

Go to ...


This page is http://www.cc.utah.edu/~nahaj/logic/checkmodal/checkmodal.perl.html
© Copyright 2001 by John Halleck, All Rights Reserved.
This snapshot was last modified on September 19th, 2001