judge-0.1.2.0: Tableau-based theorem prover.

Copyright(c) 2017 2018 N Steenbergen
LicenseGPL-3
Maintainerns@slak.ws
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Logic.Judge.Prover.Tableau

Contents

Description

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

Synopsis

Input structures

data TableauSystem ext Source #

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

Constructors

TableauSystem 

Fields

data Constraint primitive ext Source #

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

data Compositor Source #

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 Source #

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.

type RuleUninstantiated ext = Rule (Constraint PrimitiveStaticTerms ext) ext Source #

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

Term specification

data PrimitiveDynamicTerms Source #

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.

data PrimitiveStaticTerms Source #

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

Constructors

Root

Goal formula.

Assumption

Assumption formulas or constant specification.

data Terms primitive ext Source #

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) Source # 

Methods

pretty :: Terms primitive ext -> Doc Source #

prettyEmbedded :: Terms primitive ext -> Doc Source #

prettyRecursive :: Terms primitive ext -> Doc Source #

type DynamicTerms = Terms PrimitiveDynamicTerms Source #

Shorthand for a specification of complex dynamic terms.

type StaticTerms = Terms PrimitiveStaticTerms Source #

Shorthand for a specification of complex static terms.

Decision algorithm

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

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) Source #

Construct the initial branch and settings for the decision algorithm.

Intermediate structures

data TableauSettings ext Source #

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

Constructors

TableauSettings 

Fields

data Ref ref val Source #

Relates values to their identifiers.

Constructors

(:=) infixr 7 

Fields

Instances

data Branch ext Source #

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

Constructors

Branch 

Fields

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

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

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

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

Output structures

data Result input output Source #

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)) Source # 

Methods

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

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

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

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

Methods

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

data Tableau ext Source #

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) Source # 
Printable ext => LaTeX (Tableau ext) Source # 

Methods

latex :: Tableau ext -> Doc Source #

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

Methods

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

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

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

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

Methods

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

Postprocessors

shorten :: Tableau ext -> Tableau ext Source #

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 Source #

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 Source #

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 Source #

Take the first option from a list of options.

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

Take the intersection of all given lists.

combinations :: [[a]] -> [[a]] Source #

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]]