Logic.Judge.Formula.Datastructure

Plain datastructures, class instances and operations on logical formulas.

Datastructures

Formulas

data Formula ext

For our purposes, a Formula is a structure that is built upon a formula of classical propositional logic. It has all the standard connectives, plus an optional Extension that may hold quantifiers, modalities, etcetera.

Note that it is generally expected that formulas will be simplifyed before being processed.

Constructors

Variable String

Constant Bool

Extend ext (Formula ext)

Negation (Formula ext)

Conjunction (Formula ext) (Formula ext)

Disjunction (Formula ext) (Formula ext)

XDisjunction (Formula ext) (Formula ext)

Implication (Formula ext) (Formula ext)

BiImplication (Formula ext) (Formula ext)

Instances

Subterm ext ext => Subterm ext (Formula ext)

Methods

subterms :: Formula ext -> [Term ext]

Subterm ext ext => Subterm ext (Marked (Formula ext))

Methods

subterms :: Marked (Formula ext) -> [Term ext]

(Eq ext, Substitutable ext ext) => Substitutable ext (Formula ext)

Methods

substitute :: Monad m => Substitution ext -> Formula ext -> m (Formula ext)

pattern :: Monad m => Formula ext -> Formula ext -> m (Substitution ext)

patternContinue :: Monad m => Substitution ext -> Formula ext -> Formula ext -> m (Substitution ext)

patternM :: Formula ext -> Formula ext -> StateFail (Substitution ext) ()

Eq ext => Eq (Formula ext)

Methods

(==) :: Formula ext -> Formula ext -> Bool

(/=) :: Formula ext -> Formula ext -> Bool

Ord ext => Ord (Formula ext)

Methods

compare :: Formula ext -> Formula ext -> Ordering

(<) :: Formula ext -> Formula ext -> Bool

(<=) :: Formula ext -> Formula ext -> Bool

(>) :: Formula ext -> Formula ext -> Bool

(>=) :: Formula ext -> Formula ext -> Bool

max :: Formula ext -> Formula ext -> Formula ext

min :: Formula ext -> Formula ext -> Formula ext

HasVariables ext => HasVariables (Formula ext)

Methods

variables :: Formula ext -> [String]

isVariable :: Formula ext -> Bool

isConstant :: Formula ext -> Bool

isAtomary :: Formula ext -> Bool

size :: Formula ext -> Int

Parseable e => Parseable (Formula e)

Methods

parser :: Parser (Formula e)

parserEmbedded :: Parser (Formula e)

Printable ext => Printable (Formula ext)

Methods

pretty :: Formula ext -> Doc

prettyEmbedded :: Formula ext -> Doc

prettyRecursive :: Formula ext -> Doc

Printable ext => LaTeX (Formula ext)

Methods

latex :: Formula ext -> Doc

data Marked formula

A marked formula is simply a formula with zero or more string annotations. This makes for easy generalisation: marks can carry the polarity of a formula, as well as state information specific to a particular tableau system.

Constructors

Marked

Fields

• marks :: [String]
• unmarked :: formula

Instances

Functor Marked

Methods

fmap :: (a -> b) -> Marked a -> Marked b

(<$) :: a -> Marked b -> Marked a

Subterm ext ext => Subterm ext (Marked (Formula ext))

Methods

subterms :: Marked (Formula ext) -> [Term ext]

(Eq ext, Substitutable ext a) => Substitutable ext (Marked a)

Methods

substitute :: Monad m => Substitution ext -> Marked a -> m (Marked a)

pattern :: Monad m => Marked a -> Marked a -> m (Substitution ext)

patternContinue :: Monad m => Substitution ext -> Marked a -> Marked a -> m (Substitution ext)

patternM :: Marked a -> Marked a -> StateFail (Substitution ext) ()

Eq formula => Eq (Marked formula)

Methods

(==) :: Marked formula -> Marked formula -> Bool

(/=) :: Marked formula -> Marked formula -> Bool

Ord formula => Ord (Marked formula)

Methods

compare :: Marked formula -> Marked formula -> Ordering

(<) :: Marked formula -> Marked formula -> Bool

(<=) :: Marked formula -> Marked formula -> Bool

(>) :: Marked formula -> Marked formula -> Bool

(>=) :: Marked formula -> Marked formula -> Bool

max :: Marked formula -> Marked formula -> Marked formula

min :: Marked formula -> Marked formula -> Marked formula

HasVariables term => HasVariables (Marked term)

Methods

variables :: Marked term -> [String]

isVariable :: Marked term -> Bool

isConstant :: Marked term -> Bool

isAtomary :: Marked term -> Bool

size :: Marked term -> Int

Parseable f => Parseable (Marked f)

Methods

parser :: Parser (Marked f)

parserEmbedded :: Parser (Marked f)

Printable f => Printable (Marked f)

Methods

pretty :: Marked f -> Doc

prettyEmbedded :: Marked f -> Doc

prettyRecursive :: Marked f -> Doc

LaTeX a => LaTeX (Marked a)

Methods

latex :: Marked a -> Doc

data Term ext

The term datastructure disambiguates between terms of the logical language and terms of the logical extension language (e.g. justifications).

The alternative to carrying this information at the value level is to have a multi-parameter Substructure sub base class relative to which operations like patterning or the occurs check are defined. Although that seemed prettier in theory, it made the code a whole lot more complicated.

Constructors

Formula (Formula ext)

Extension ext

MarkedFormula (Marked (Formula ext))

Instances

Subterm ext ext => Subterm ext (Ambiguous (Term ext))

Methods

subterms :: Ambiguous (Term ext) -> [Term ext]

Subterm ext ext => Subterm ext (Term ext)

Methods

subterms :: Term ext -> [Term ext]

(Eq ext, Substitutable ext ext) => Substitutable ext (Term ext)

Methods

substitute :: Monad m => Substitution ext -> Term ext -> m (Term ext)

pattern :: Monad m => Term ext -> Term ext -> m (Substitution ext)

patternContinue :: Monad m => Substitution ext -> Term ext -> Term ext -> m (Substitution ext)

patternM :: Term ext -> Term ext -> StateFail (Substitution ext) ()

Eq ext => Eq (Term ext)

Methods

(==) :: Term ext -> Term ext -> Bool

(/=) :: Term ext -> Term ext -> Bool

Ord ext => Ord (Term ext)

Methods

compare :: Term ext -> Term ext -> Ordering

(<) :: Term ext -> Term ext -> Bool

(<=) :: Term ext -> Term ext -> Bool

(>) :: Term ext -> Term ext -> Bool

(>=) :: Term ext -> Term ext -> Bool

max :: Term ext -> Term ext -> Term ext

min :: Term ext -> Term ext -> Term ext

HasVariables ext => HasVariables (Ambiguous (Term ext))

Methods

variables :: Ambiguous (Term ext) -> [String]

isVariable :: Ambiguous (Term ext) -> Bool

isConstant :: Ambiguous (Term ext) -> Bool

isAtomary :: Ambiguous (Term ext) -> Bool

size :: Ambiguous (Term ext) -> Int

HasVariables ext => HasVariables (Term ext)

Methods

variables :: Term ext -> [String]

isVariable :: Term ext -> Bool

isConstant :: Term ext -> Bool

isAtomary :: Term ext -> Bool

size :: Term ext -> Int

Parseable e => Parseable (Ambiguous (Term e))

Methods

parser :: Parser (Ambiguous (Term e))

parserEmbedded :: Parser (Ambiguous (Term e))

Printable ext => Printable (Term ext)

Methods

pretty :: Term ext -> Doc

prettyEmbedded :: Term ext -> Doc

prettyRecursive :: Term ext -> Doc

newtype Ambiguous term

A parsed term may be ambiguous: S can be parsed as a Formula or as a Justification. Such ambiguous are stored in an Ambiguous type to be resolved later.

Constructors

Ambiguous [term]

Instances

Subterm ext ext => Subterm ext (Ambiguous (Term ext))

Methods

subterms :: Ambiguous (Term ext) -> [Term ext]

HasVariables ext => HasVariables (Ambiguous (Term ext))

Methods

variables :: Ambiguous (Term ext) -> [String]

isVariable :: Ambiguous (Term ext) -> Bool

isConstant :: Ambiguous (Term ext) -> Bool

isAtomary :: Ambiguous (Term ext) -> Bool

size :: Ambiguous (Term ext) -> Int

Parseable e => Parseable (Ambiguous (Term e))

Methods

parser :: Parser (Ambiguous (Term e))

parserEmbedded :: Parser (Ambiguous (Term e))

Printable term => Printable (Ambiguous term)

Methods

pretty :: Ambiguous term -> Doc

prettyEmbedded :: Ambiguous term -> Doc

prettyRecursive :: Ambiguous term -> Doc

Extensions

type Proposition = Formula Classical

Formulas of propositional logic.

type Predicate = Formula Quantifier

Formulas of predicate logic.

type FormulaML = Formula Modality

Formulas of modal logic.

type FormulaJL = Formula Justification

Formulas of justification logic.

type Classical = ()

The formula extension for classical propositional logic is empty.

data Quantifier

Predicate logic is extended with quantifiers (and relation symbols, unimplemented).

Constructors

Universal String

Existential String

Instances

Eq Quantifier

Methods

(==) :: Quantifier -> Quantifier -> Bool

(/=) :: Quantifier -> Quantifier -> Bool

Parseable Quantifier

Methods

parser :: Parser Quantifier

parserEmbedded :: Parser Quantifier

Printable Quantifier

Methods

pretty :: Quantifier -> Doc

prettyEmbedded :: Quantifier -> Doc

prettyRecursive :: Quantifier -> Doc

data Modality

Standard modal logics have two (dual) unary modal operators.

Constructors

Necessary

Possible

Instances

Eq Modality

Methods

(==) :: Modality -> Modality -> Bool

(/=) :: Modality -> Modality -> Bool

Ord Modality

Methods

compare :: Modality -> Modality -> Ordering

(<) :: Modality -> Modality -> Bool

(<=) :: Modality -> Modality -> Bool

(>) :: Modality -> Modality -> Bool

(>=) :: Modality -> Modality -> Bool

max :: Modality -> Modality -> Modality

min :: Modality -> Modality -> Modality

Parseable Modality

Methods

parser :: Parser Modality

parserEmbedded :: Parser Modality

Printable Modality

Methods

pretty :: Modality -> Doc

prettyEmbedded :: Modality -> Doc

prettyRecursive :: Modality -> Doc

data Justification

Justification logics are extended with justification terms.

Constructors

ProofVariable String

ProofConstant String

ProofChecker Justification

Application Justification Justification

Sum Justification Justification

Instances

Eq Justification

Methods

(==) :: Justification -> Justification -> Bool

(/=) :: Justification -> Justification -> Bool

Ord Justification

Methods

compare :: Justification -> Justification -> Ordering

(<) :: Justification -> Justification -> Bool

(<=) :: Justification -> Justification -> Bool

(>) :: Justification -> Justification -> Bool

(>=) :: Justification -> Justification -> Bool

max :: Justification -> Justification -> Justification

min :: Justification -> Justification -> Justification

HasVariables Justification

Methods

variables :: Justification -> [String]

isVariable :: Justification -> Bool

isConstant :: Justification -> Bool

isAtomary :: Justification -> Bool

size :: Justification -> Int

Parseable Justification

Methods

parser :: Parser Justification

parserEmbedded :: Parser Justification

Extension Justification

Printable Justification

Methods

pretty :: Justification -> Doc

prettyEmbedded :: Justification -> Doc

prettyRecursive :: Justification -> Doc

Subterm Justification Justification

Methods

subterms :: Justification -> [Term Justification]

Substitutable Justification Justification

Methods

substitute :: Monad m => Substitution Justification -> Justification -> m Justification

pattern :: Monad m => Justification -> Justification -> m (Substitution Justification)

patternContinue :: Monad m => Substitution Justification -> Justification -> Justification -> m (Substitution Justification)

patternM :: Justification -> Justification -> StateFail (Substitution Justification) ()

Operations

simplify :: Formula ext -> Formula ext

Simplify formulae to only falsehood, implication and justification. This reduces the number of rules that need implementation.

asTerm :: Marked (Formula ext) -> [Term ext]

Interpret a marked formula as a choice of terms. Note that it is not always clear whether a value from Terms is meant as the marked or the unmarked version — so we offer both.

isFormula :: Term ext -> Bool

Return true if and only if the term is a formula.

isExtension :: Term ext -> Bool

Return true iff the term is a formula extension.

isMarkedFormula :: Term ext -> Bool

Return true iff the term is a marked formula.

Classes

class Subterm ext term where

The Subterm class represents a relation between terms based on an extension ext (that is, formulas or extensions of formulas) and subterms that may occur within those ext-terms.

Minimal complete definition

subterms

Methods

subterms :: term -> [Term ext]

Return all the subterms occurring in a term. Note: May contain duplicates.

Instances

Subterm Justification Justification

Methods

subterms :: Justification -> [Term Justification]

Subterm ext ext => Subterm ext (Formula ext)

Methods

subterms :: Formula ext -> [Term ext]

Subterm ext ext => Subterm ext (Ambiguous (Term ext))

Methods

subterms :: Ambiguous (Term ext) -> [Term ext]

Subterm ext ext => Subterm ext (Marked (Formula ext))

Methods

subterms :: Marked (Formula ext) -> [Term ext]

Subterm ext ext => Subterm ext (Term ext)

Methods

subterms :: Term ext -> [Term ext]

class HasVariables term where

The HasVariables class is applicable to formulas and formula extensions that consist of substructures with variables and constants, and operators to combine them.

Minimal complete definition

variables, isVariable, isConstant, size

Methods

variables :: term -> [String]

Return the variables occurring in a term. Note: May contain duplicates.

isVariable :: term -> Bool

Return true if the term is a variable.

isConstant :: term -> Bool

Return true if the term is a constant.

isAtomary :: term -> Bool

Return true if the term is atomary.

size :: term -> Int

Return the number of operators in the term.

Instances

HasVariables Justification

Methods

variables :: Justification -> [String]

isVariable :: Justification -> Bool

isConstant :: Justification -> Bool

isAtomary :: Justification -> Bool

size :: Justification -> Int

HasVariables ext => HasVariables (Ambiguous (Term ext))

Methods

variables :: Ambiguous (Term ext) -> [String]

isVariable :: Ambiguous (Term ext) -> Bool

isConstant :: Ambiguous (Term ext) -> Bool

isAtomary :: Ambiguous (Term ext) -> Bool

size :: Ambiguous (Term ext) -> Int

HasVariables ext => HasVariables (Term ext)

Methods

variables :: Term ext -> [String]

isVariable :: Term ext -> Bool

isConstant :: Term ext -> Bool

isAtomary :: Term ext -> Bool

size :: Term ext -> Int

HasVariables term => HasVariables (Marked term)

Methods

variables :: Marked term -> [String]

isVariable :: Marked term -> Bool

isConstant :: Marked term -> Bool

isAtomary :: Marked term -> Bool

size :: Marked term -> Int

HasVariables ext => HasVariables (Formula ext)

Methods

variables :: Formula ext -> [String]

isVariable :: Formula ext -> Bool

isConstant :: Formula ext -> Bool

isAtomary :: Formula ext -> Bool

size :: Formula ext -> Int