Lotrecscheme
This
software enables to develop a tableau method for a logic quickly. You
design tableau rules with pattern-matching graphically. You can use the
programming language Scheme for subtle conditions or subtle actions to
apply in your tableau method and also to write your formulas.
Formulas are written in Scheme way: p, (diamond q), (atlbox (1 3 2) (p or q))...
You can not write diamond(p or q).... you need to give all the parenthesis: (diamond (p or q)).
A rule is made up of a left hand-side (condition) and... zero, one or two left hand-side(s).
Edit the left hand-side
Edit the right hand-side
Manage the set of rules
API Scheme
Integer
Kripke model
Formula
Sets
Lists