greati / logicantsy Goto Github PK

Demands to vary the set of designated values, as well as each interpretation.

• input: pure and simple sequents, fully non-deterministic table
• output possibly deterministic table for which the input sequents are not counter-models

In JB's work, this is in a "logica" class. Indeed, this set of separators induces the general axiomatization for the corresponding PN-matrix.

Take a formula and a map from variables to formulas and perform a uniform substitution.

Implement LaTeX representations for:

• Formulas
• NdSequents
• Truth Tables

Mainly the cases where parentheses are used for precedence order change.

• collect all propositional variables occurring in the formula
• infer the (least) signature of the language of a given formula

Based on Batista's algorithm.

Decouple

• MultipleConclusionCalculus
• ProofSearchStrategy
• RuleInstanceSelectionHeuristics

• Allow a truth table to provide its list of determinants
• Allow to easily retrieve the last value of a determinant, as well as its other values

Important: provide it in slots, preparing for the implementation of B-entailment axiomatizatiions.

Should this be a new class or an special case of NdSequentRules?

• generator for valuations over a PNmatrix
• allow to pass a sub-signature to a generator, allowing this to produce interpretations for the connectives which appear in the rule

I forgot to do the union.