Logic.Judge.Prover.Tableau

A generic decision algorithm based on the method of analytic tableaux.

Input structures

data TableauSystem ext

Before initialisation, the tableau system is read into this structure.

Constructors

TableauSystem

Fields

• title :: String
• rules :: [RuleUninstantiated ext]
• assumptions' :: [Formula ext]

Instances

Printable ext => Printable (TableauSystem ext)

Methods

pretty :: TableauSystem ext -> Doc

prettyEmbedded :: TableauSystem ext -> Doc

prettyRecursive :: TableauSystem ext -> Doc

data Constraint primitive ext

A constraint is placed on a tableau rule to restrict the values to which its variables can be bound. This means that some applications of the rule will be blocked; but also that any "free" or "generative" variables (that is, variables that occur in the rule's productions but not in its consumptions) can now be associated with a set of possible assignments, thereby making it possible to, essentially, generate a choice of multiple instantiations of a single rule.

Constructors

None

Bind (Ambiguous (Term ext)) (Terms primitive ext)

Demand that the pattern occurs in a particular set of terms.

Choose [Constraint primitive ext]

Constraint holds if one of the subconstraints hold.

Merge [Constraint primitive ext]

Constraint holds if all subconstraints hold.

Instances

Printable ext => Printable (RuleUninstantiated ext)

Methods

pretty :: RuleUninstantiated ext -> Doc

prettyEmbedded :: RuleUninstantiated ext -> Doc

prettyRecursive :: RuleUninstantiated ext -> Doc

(Printable ext, Printable primitive) => Printable (Constraint primitive ext)

Methods

pretty :: Constraint primitive ext -> Doc

prettyEmbedded :: Constraint primitive ext -> Doc

prettyRecursive :: Constraint primitive ext -> Doc

data Compositor

Indicates how to handle the situation where multiple rule instantiations are applicable to the same formula.

Due to their computational complexity, rules that do not take any consumptions are handled greedily regardless of the value of the compositor.

Constructors

Greedy

Nondeterministic

data Rule generator ext

A rule describes which formulas it consumes and which it produces. In its basic form, it can represent both instantiated and uninstantiated tableau rules (see RuleInstantiated and RuleUninstantiated).

Constructors

Rule

Fields

• name :: String

  Identifier by which the rule shall be known.

• consumptions :: [Marked (Formula ext)]

  The consumptions (also: premises, antecedents, conditions) are formulas that are to be present on the branch before the rule may be applied.

• productions :: [[Marked (Formula ext)]]

  The productions (also: conclusions, consequents, results) are the formulas that will be created on the branch when the rule is applied. Represents a disjunction of conjunctions.

• generator :: generator

  A generator is a "permissive constraint", which represents a choice between possible variable assignments. This approach is necessary to be able to handle free variables in the productions: such variables do not have a pre-existing binding to check for compliance, so they need to be created. This also makes it possible to keep track of which bindings have already been attempted over the course of an algorithm, thus allowing for termination guarantees in case termination is not certain otherwise.

  The limitation of the generator is that it is not very efficient and that no variable may be bound to terms from a dynamic set, since the generator has to generate its instances at the beginning of the algorithm. (Note that the last point can be dropped if we do not need to keep track of which bindings have already been used.)

• constraint :: Constraint PrimitiveDynamicTerms ext

  Although the generator does also restrict bound variables (with brute force: a variable's previous binding will block all conflicting assignments), it is more computationally efficient to simply check already known values for compliance, during runtime.

  The limitation of restrictive constraints is that they cannot deal with free variables.

• compositor :: Compositor

  The compositor indicates how to handle the case where multiple instances are suggested by the generator.

Instances

Printable ext => Printable (RuleUninstantiated ext)

Methods

pretty :: RuleUninstantiated ext -> Doc

prettyEmbedded :: RuleUninstantiated ext -> Doc

prettyRecursive :: RuleUninstantiated ext -> Doc

type RuleUninstantiated ext = Rule (Constraint PrimitiveStaticTerms ext) ext

Before instantiation, a generator is described by a constraint. This constraint can only refer to static terms.

Term specification

data PrimitiveDynamicTerms

Represent sets of primitive source formulas to be used in restrictive constraints.

Constructors

Static PrimitiveStaticTerms

Processed

Active terms, currently not processed on the branch.

Unprocessed

Inactive terms, currently processed on the branch.

Instances

Printable PrimitiveDynamicTerms

Methods

pretty :: PrimitiveDynamicTerms -> Doc

prettyEmbedded :: PrimitiveDynamicTerms -> Doc

prettyRecursive :: PrimitiveDynamicTerms -> Doc

data PrimitiveStaticTerms

Represent sets of primitive source formulas to be used in generators and restrictive constraints.

Constructors

Root

Goal formula.

Assumption

Assumption formulas or constant specification.

Instances

Printable PrimitiveStaticTerms

Methods

pretty :: PrimitiveStaticTerms -> Doc

prettyEmbedded :: PrimitiveStaticTerms -> Doc

prettyRecursive :: PrimitiveStaticTerms -> Doc

Printable ext => Printable (RuleUninstantiated ext)

Methods

pretty :: RuleUninstantiated ext -> Doc

prettyEmbedded :: RuleUninstantiated ext -> Doc

prettyRecursive :: RuleUninstantiated ext -> Doc

data Terms primitive ext

Represent complex sets of source terms, to be turned into concrete terms at a point where it is known what they should refer to. Static terms are known at the start of the tableau procedure, whereas dynamic terms should be evaluated dynamically.

Constructors

Primitive primitive

Union [Terms primitive ext]

Keep terms that occur in at least one constituent.

Intersection [Terms primitive ext]

Keep only terms that occur in all constituents.

Transform String ([Term ext] -> [Term ext]) (Terms primitive ext)

Apply a transformation to terms.

Instances

(Printable ext, Printable primitive) => Printable (Terms primitive ext)

Methods

pretty :: Terms primitive ext -> Doc

prettyEmbedded :: Terms primitive ext -> Doc

prettyRecursive :: Terms primitive ext -> Doc

type DynamicTerms = Terms PrimitiveDynamicTerms

Shorthand for a specification of complex dynamic terms.

type StaticTerms = Terms PrimitiveStaticTerms

Shorthand for a specification of complex static terms.

Decision algorithm

decide :: forall ext. Extension ext => TableauSystem ext -> Formula ext -> Result (Formula ext) (Tableau ext)

Decide the validity of the target formula within the given logical system. A branch closes when it internally contradicts. A branch that is neither closed nor expandable corresponds to a satisfying assignment of the negation of the target formula, and constitutes a counter-model. Otherwise, we have successfully shown the formula's validity and can return a Tableau.

initial :: forall ext. Extension ext => TableauSystem ext -> Formula ext -> (TableauSettings ext, Branch ext)

Construct the initial branch and settings for the decision algorithm.

Intermediate structures

data TableauSettings ext

The global state of the tableau — settings that will remain static after initialisation.

Constructors

TableauSettings

Fields

• rulesC :: [RuleInstantiated ext]

  The consumer rules are those rules that take a consumption from the branch. They are always available.

• root :: Marked (Formula ext)

  The root of the tableau.

• assumptions :: [Formula ext]

  The assumptions or the constant specification.

data Ref ref val

Relates values to their identifiers.

Constructors

(:=) infixr 7

Fields

• reference :: ref
• value :: val

Instances

Printable b => Printable (Ref Int b)

Methods

pretty :: Ref Int b -> Doc

prettyEmbedded :: Ref Int b -> Doc

prettyRecursive :: Ref Int b -> Doc

LaTeX a => LaTeX (Ref Int a)

Methods

latex :: Ref Int a -> Doc

data Branch ext

A Branch keeps track of the leaf of a single branch of the tableau, and all that came before.

Constructors

Branch

Fields

• rulesA :: Maybe (PointedList (RuleInstantiated ext))

  The ascetic rules are those rules that do not take a consumption from the branch. In order to guarantee termination, they can be used only once per branch — we therefore keep track of which rules can still be used.

• actives :: Maybe (PointedList (BranchFormula ext))

  Which formulas still lie unprocessed on the branch?

• inactives :: [BranchFormula ext]

  Which formulas have been processed on the branch?

• new :: [BranchFormula ext]

  Which formulas were the last to be introduced?

• counter :: Int

  The next identifier never to have occurred on the branch before.

type BranchFormula ext = Ref Int (Marked (Formula ext))

Formulas on the branch are decorated by their reference number and marks.

type RuleInstantiated ext = Rule (PointedList (Substitution ext)) ext

After instantiation, a generator consists of all variable assignments that it allows.

Output structures

data Result input output

Like Either, but remembers the original input in the Right case, too.

Constructors

Success input output

Failure input

Instances

(Printable input, Printable ext) => Printable (Result input (Tableau ext))

Methods

pretty :: Result input (Tableau ext) -> Doc

prettyEmbedded :: Result input (Tableau ext) -> Doc

prettyRecursive :: Result input (Tableau ext) -> Doc

(LaTeX input, Printable ext) => LaTeX (Result input (Tableau ext))

Methods

latex :: Result input (Tableau ext) -> Doc

data Tableau ext

A proof in a tableau system is a rose tree, containing sets of formulas and the rule applications used to obtain them.

Constructors

Node [BranchFormula ext] (Tableau ext)

Application String [Int] [Tableau ext]

Closure [Int]

Instances

Printable ext => Printable (Tableau ext)

Methods

pretty :: Tableau ext -> Doc

prettyEmbedded :: Tableau ext -> Doc

prettyRecursive :: Tableau ext -> Doc

Printable ext => LaTeX (Tableau ext)

Methods

latex :: Tableau ext -> Doc

(Printable input, Printable ext) => Printable (Result input (Tableau ext))

Methods

pretty :: Result input (Tableau ext) -> Doc

prettyEmbedded :: Result input (Tableau ext) -> Doc

prettyRecursive :: Result input (Tableau ext) -> Doc

(LaTeX input, Printable ext) => LaTeX (Result input (Tableau ext))

Methods

latex :: Result input (Tableau ext) -> Doc

Postprocessors

shorten :: Tableau ext -> Tableau ext

Eliminate rule applications that do not produce any formulas that are involved in closing any branch.

Note that this will not eliminate all unnecessary applications (let alone find the shortest proof) — it will only remove rules that are not involved in any closure. For example, for justification logic, if c:φ and d:ψ are in the CS but only d:ψ has to be introduced via CSr, then this will remove any redundant CSr application — but if a formula is introduced via a restricted cut, it could do nothing because the cut-formula IS involved in the closure of a branch, even though it was pointless to do the cut in the first place. It would be nice to think of a stronger method.

renumber :: Int -> Tableau ext -> Tableau ext

Make the reference numbers on the formulas heterogeneous, even if they are on different branches. This is done in a single step at the end so that we do not have the mental (and computational) burden of carrying a State monad everywhere.

rewrite :: Extension ext => Formula ext -> Tableau ext -> Tableau ext

If the root formula is not exactly equal to the input formula, there was supposedly a rewriting step. Add this step to the tableau explicitly, to show what happened.

Auxiliaries

greedy :: Alternative f => [a] -> f a

Take the first option from a list of options.

intersection :: Eq a => [[a]] -> [a]

Take the intersection of all given lists.

combinations :: [[a]] -> [[a]]

A variation on permutations: given a list that describes the possible elements at each position, give all possible element combinations. In a sense, this is a transpose operation.

Example: [[1,2],[3,4]] -> [[1,3],[1,4],[2,3],[2,4]]