A computational algorithm for the verification of tautologies in propositional calculus

Abstract

A computational  algorithm (based on  Snlullyan's  analytic  tableau  method)  that  verifies  whether  a  given  well formed  formula  in  propositional  calculus  is  a  tautology  or  not  has  been  implemented  on  a  DEC  System 10.  The  stepwise  refinement  approach  of  program development  used  for  this  implementation  forms  the  subject  matter  of  this  paper.  This  top-down design  has  resulted  in  a  modular  and  reliable  program  package.  This computational  algorithm  compares  favourably  with  the  algorithm  based  on  the  well-known  resolution  principle  used in  theorem  provers.