ModaLogic Architecture Documentation¶
The Tableau Feature¶
Our process for evaluating modal logic arguments is centered around the analytical tableau method. This method uses the de-compositional approach to the evaluation of the from argument. This means the procedure works from the argument level down as opposed to the axiomatic methods that aim to build the argument up from axioms.
The technical implementation of the analytical tableau method is thus based on the definition of a tree structure that represents the argument. The first node at the root being the argument to evaluate, the second the negation of that argument and then for all lower "branches" of the tree we execute the tree construction process to see if the tableau closes (all branches end in inconstencies: proving the validaity of the original statement) or if some branch stays open which disproves the original statement.
The analytical table creation process uses a well-defined series of replacement rules depending on the type of logic system that is beig evaluated. For the implementation process of the modalogic processor we will progressively develop the scope of supported logic systems, starting with common propositional logic argument. We will progress through predicate first order logic with quantitications and then move into supporting the various modal logic systems.
This is a progression that can be build sequentially as each of the later logic systems builds on the lower systems. As we get into the modal logic systems we get into disjunct sets of replacement rules at which point the user will need to specify the logic system to use which will then activate which replacement and world-access rules will be activated for the evaluation.
The main progression for the logic systems support: * propositional logic * predicate logic with quantifiers * predicate logic with function unification * modal logic K-system * derived modal primary logic systems like S1-S5 etc. * first order modal logic systems * MODFOL with equality, etc.
Systemic Tableau Construction¶
The Tableau is a simple datastructure that consists of TableaNodes. This structure has no self-awareness of how to manage its content. The blackboard is the component that has the knowledge about the creation procedures for the tableau and which of the logic systems is needed to evaluate the argument.
So the construction of the evaluation context involves three main The parser doesn't know anything about the nodes so to construct the table we have to wrapp all the formulas that the parser might return (premises and/or conclusion formula) into TableauNodes. The information to do so comes from the ArgumentParser that has access to the parsers of each of the optional premises and the parser of the required conclusion.
In the test files we start with the verification that the TableauNodes are constructed correctly and then proceed to the construction of the initial Tableau.