Re: Richard J. Lipton • Logical Complexity Of Proofs

The smoothest way I know to do propositional calculus is by using minimal negation operators as primitives, parsing propositional formulas into (painted and rooted) cactus graphs, and using the appropriate extension of the axiom set from Charles S. Peirce’s logical graphs and G. Spencer Brown’s laws of form.  There’s a quick link here:

• Cactus Language for Propositional Logic

Resources

• Logic Syllabus
• Logical Graphs
• Cactus Language
• Futures Of Logical Graphs
• Minimal Negation Operators
• Survey of Theme One Program
• Survey of Animated Logical Graphs
• Propositional Equation Reasoning Systems

Applications

• Applications of a Propositional Calculator • Constraint Satisfaction Problems
• Exploratory Qualitative Analysis of Sequential Observation Data

cc: Cybernetics • Ontolog • Peirce (1) (2) (3) (4) (5) (6) • Structural Modeling • Systems