A visual logic
John R. Fisher, Luu Tran · 1996
Logic programs with classical negation are defined• The analysis of these programs is based in a fundamental way upon the theory of sets of disjunctive clauses, which was the basis of theorem-proving theory in the 1960s and early 1970s.Like arbitrary sets of disjunctive clauses, these logic programs can be classically inconsistent, or unsatisfiable.Although such programs may be classically trivial (every proposition is a theorem), this need not be the case for interesting subprograms.The paper motivates and defines the concept of a supported proposition, using definitions based upon clause trees.Supported propositions are supposed to be relatively safe logical consequences of certain consistent subprograms.To effectively use these definitions for practical application --and, indeed, to effectively present the concepts for consideration in the first place --requires some intuitive, form of visualization.To this end the authors use a "visual logic" tool (the one in the title) to illustrate the examples for the basic definitions of the paper.Thus, the paper uses (a preliminary version of) the visual tool to explain the theory that justifies the tool.The final section gives a brief discussion of visual logic more generally. CLAUSESA disjunctive clause has the form Liv L2 v... v Ln where the Li are literals, n>= O.When n=0, the clause is the empty clause, referred to as nil.