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