Copyright	(c) 2017 2018 N Steenbergen
License	GPL-3
Maintainer	ns@slak.ws
Stability	experimental
Safe Haskell	Safe
Language	Haskell2010

Logic.Judge.Formula.Datastructure

Contents

Datastructures
- Formulas
- Extensions
Operations
Classes

Description

Plain datastructures, class instances and operations on logical formulas.

Synopsis

Datastructures

Formulas

data Formula ext Source #

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) Source #
Methods subterms :: Formula ext -> [Term ext] Source #
Subterm ext ext => Subterm ext (Marked (Formula ext)) Source #
Methods subterms :: Marked (Formula ext) -> [Term ext] Source #
(Eq ext, Substitutable ext ext) => Substitutable ext (Formula ext) Source #
Methods substitute :: Monad m => Substitution ext -> Formula ext -> m (Formula ext) Source # pattern :: Monad m => Formula ext -> Formula ext -> m (Substitution ext) Source # patternContinue :: Monad m => Substitution ext -> Formula ext -> Formula ext -> m (Substitution ext) Source # patternM :: Formula ext -> Formula ext -> StateFail (Substitution ext) ()
Eq ext => Eq (Formula ext) Source #
Methods (==) :: Formula ext -> Formula ext -> Bool # (/=) :: Formula ext -> Formula ext -> Bool #
Ord ext => Ord (Formula ext) Source #
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) Source #
Methods variables :: Formula ext -> [String] Source # isVariable :: Formula ext -> Bool Source # isConstant :: Formula ext -> Bool Source # isAtomary :: Formula ext -> Bool Source # size :: Formula ext -> Int Source #
Parseable e => Parseable (Formula e) Source #
Methods parser :: Parser (Formula e) Source # parserEmbedded :: Parser (Formula e) Source #
Printable ext => Printable (Formula ext) Source #
Methods pretty :: Formula ext -> Doc Source # prettyEmbedded :: Formula ext -> Doc Source # prettyRecursive :: Formula ext -> Doc Source #
Printable ext => LaTeX (Formula ext) Source #
Methods latex :: Formula ext -> Doc Source #

data Marked formula Source #

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 Source #
Methods fmap :: (a -> b) -> Marked a -> Marked b # (<$) :: a -> Marked b -> Marked a #
Subterm ext ext => Subterm ext (Marked (Formula ext)) Source #
Methods subterms :: Marked (Formula ext) -> [Term ext] Source #
(Eq ext, Substitutable ext a) => Substitutable ext (Marked a) Source #
Methods substitute :: Monad m => Substitution ext -> Marked a -> m (Marked a) Source # pattern :: Monad m => Marked a -> Marked a -> m (Substitution ext) Source # patternContinue :: Monad m => Substitution ext -> Marked a -> Marked a -> m (Substitution ext) Source # patternM :: Marked a -> Marked a -> StateFail (Substitution ext) ()
Eq formula => Eq (Marked formula) Source #
Methods (==) :: Marked formula -> Marked formula -> Bool # (/=) :: Marked formula -> Marked formula -> Bool #
Ord formula => Ord (Marked formula) Source #
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) Source #
Methods variables :: Marked term -> [String] Source # isVariable :: Marked term -> Bool Source # isConstant :: Marked term -> Bool Source # isAtomary :: Marked term -> Bool Source # size :: Marked term -> Int Source #
Parseable f => Parseable (Marked f) Source #
Methods parser :: Parser (Marked f) Source # parserEmbedded :: Parser (Marked f) Source #
Printable f => Printable (Marked f) Source #
Methods pretty :: Marked f -> Doc Source # prettyEmbedded :: Marked f -> Doc Source # prettyRecursive :: Marked f -> Doc Source #
LaTeX a => LaTeX (Marked a) Source #
Methods latex :: Marked a -> Doc Source #

data Term ext Source #

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)) Source #
Methods subterms :: Ambiguous (Term ext) -> [Term ext] Source #
Subterm ext ext => Subterm ext (Term ext) Source #
Methods subterms :: Term ext -> [Term ext] Source #
(Eq ext, Substitutable ext ext) => Substitutable ext (Term ext) Source #
Methods substitute :: Monad m => Substitution ext -> Term ext -> m (Term ext) Source # pattern :: Monad m => Term ext -> Term ext -> m (Substitution ext) Source # patternContinue :: Monad m => Substitution ext -> Term ext -> Term ext -> m (Substitution ext) Source # patternM :: Term ext -> Term ext -> StateFail (Substitution ext) ()
Eq ext => Eq (Term ext) Source #
Methods (==) :: Term ext -> Term ext -> Bool # (/=) :: Term ext -> Term ext -> Bool #
Ord ext => Ord (Term ext) Source #
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)) Source #
Methods variables :: Ambiguous (Term ext) -> [String] Source # isVariable :: Ambiguous (Term ext) -> Bool Source # isConstant :: Ambiguous (Term ext) -> Bool Source # isAtomary :: Ambiguous (Term ext) -> Bool Source # size :: Ambiguous (Term ext) -> Int Source #
HasVariables ext => HasVariables (Term ext) Source #
Methods variables :: Term ext -> [String] Source # isVariable :: Term ext -> Bool Source # isConstant :: Term ext -> Bool Source # isAtomary :: Term ext -> Bool Source # size :: Term ext -> Int Source #
Parseable e => Parseable (Ambiguous (Term e)) Source #
Methods parser :: Parser (Ambiguous (Term e)) Source # parserEmbedded :: Parser (Ambiguous (Term e)) Source #
Printable ext => Printable (Term ext) Source #
Methods pretty :: Term ext -> Doc Source # prettyEmbedded :: Term ext -> Doc Source # prettyRecursive :: Term ext -> Doc Source #

newtype Ambiguous term Source #

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)) Source #
Methods subterms :: Ambiguous (Term ext) -> [Term ext] Source #
HasVariables ext => HasVariables (Ambiguous (Term ext)) Source #
Methods variables :: Ambiguous (Term ext) -> [String] Source # isVariable :: Ambiguous (Term ext) -> Bool Source # isConstant :: Ambiguous (Term ext) -> Bool Source # isAtomary :: Ambiguous (Term ext) -> Bool Source # size :: Ambiguous (Term ext) -> Int Source #
Parseable e => Parseable (Ambiguous (Term e)) Source #
Methods parser :: Parser (Ambiguous (Term e)) Source # parserEmbedded :: Parser (Ambiguous (Term e)) Source #
Printable term => Printable (Ambiguous term) Source #
Methods pretty :: Ambiguous term -> Doc Source # prettyEmbedded :: Ambiguous term -> Doc Source # prettyRecursive :: Ambiguous term -> Doc Source #

Extensions

type Proposition = Formula Classical Source #

Formulas of propositional logic.

type Predicate = Formula Quantifier Source #

Formulas of predicate logic.

type FormulaML = Formula Modality Source #

Formulas of modal logic.

type FormulaJL = Formula Justification Source #

Formulas of justification logic.

type Classical = () Source #

The formula extension for classical propositional logic is empty.

data Quantifier Source #

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

Constructors

Universal String
Existential String

Instances

Eq Quantifier Source #
Methods (==) :: Quantifier -> Quantifier -> Bool # (/=) :: Quantifier -> Quantifier -> Bool #
Parseable Quantifier Source #
Methods parser :: Parser Quantifier Source # parserEmbedded :: Parser Quantifier Source #
Printable Quantifier Source #
Methods pretty :: Quantifier -> Doc Source # prettyEmbedded :: Quantifier -> Doc Source # prettyRecursive :: Quantifier -> Doc Source #

data Modality Source #

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

Constructors

Necessary
Possible

Instances

Eq Modality Source #
Methods (==) :: Modality -> Modality -> Bool # (/=) :: Modality -> Modality -> Bool #
Ord Modality Source #
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 Source #
Methods parser :: Parser Modality Source # parserEmbedded :: Parser Modality Source #
Printable Modality Source #
Methods pretty :: Modality -> Doc Source # prettyEmbedded :: Modality -> Doc Source # prettyRecursive :: Modality -> Doc Source #

data Justification Source #

Justification logics are extended with justification terms.

Constructors

ProofVariable String
ProofConstant String
ProofChecker Justification
Application Justification Justification
Sum Justification Justification

Instances

Eq Justification Source #
Methods (==) :: Justification -> Justification -> Bool # (/=) :: Justification -> Justification -> Bool #
Ord Justification Source #
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 Source #
Methods variables :: Justification -> [String] Source # isVariable :: Justification -> Bool Source # isConstant :: Justification -> Bool Source # isAtomary :: Justification -> Bool Source # size :: Justification -> Int Source #
Parseable Justification Source #
Methods parser :: Parser Justification Source # parserEmbedded :: Parser Justification Source #
Extension Justification Source #

Printable Justification Source #
Methods pretty :: Justification -> Doc Source # prettyEmbedded :: Justification -> Doc Source # prettyRecursive :: Justification -> Doc Source #
Subterm Justification Justification Source #
Methods subterms :: Justification -> [Term Justification] Source #
Substitutable Justification Justification Source #
Methods substitute :: Monad m => Substitution Justification -> Justification -> m Justification Source # pattern :: Monad m => Justification -> Justification -> m (Substitution Justification) Source # patternContinue :: Monad m => Substitution Justification -> Justification -> Justification -> m (Substitution Justification) Source # patternM :: Justification -> Justification -> StateFail (Substitution Justification) ()

Operations

simplify :: Formula ext -> Formula ext Source #

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

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

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

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

isExtension :: Term ext -> Bool Source #

Return true iff the term is a formula extension.

isMarkedFormula :: Term ext -> Bool Source #

Return true iff the term is a marked formula.

Classes

class Subterm ext term where Source #

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

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

Instances

Subterm Justification Justification Source #
Methods subterms :: Justification -> [Term Justification] Source #
Subterm ext ext => Subterm ext (Formula ext) Source #
Methods subterms :: Formula ext -> [Term ext] Source #
Subterm ext ext => Subterm ext (Ambiguous (Term ext)) Source #
Methods subterms :: Ambiguous (Term ext) -> [Term ext] Source #
Subterm ext ext => Subterm ext (Marked (Formula ext)) Source #
Methods subterms :: Marked (Formula ext) -> [Term ext] Source #
Subterm ext ext => Subterm ext (Term ext) Source #
Methods subterms :: Term ext -> [Term ext] Source #

class HasVariables term where Source #

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

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

isVariable :: term -> Bool Source #

Return true if the term is a variable.

isConstant :: term -> Bool Source #

Return true if the term is a constant.

isAtomary :: term -> Bool Source #

Return true if the term is atomary.

size :: term -> Int Source #

Return the number of operators in the term.

Instances

HasVariables Justification Source #
Methods variables :: Justification -> [String] Source # isVariable :: Justification -> Bool Source # isConstant :: Justification -> Bool Source # isAtomary :: Justification -> Bool Source # size :: Justification -> Int Source #
HasVariables ext => HasVariables (Ambiguous (Term ext)) Source #
Methods variables :: Ambiguous (Term ext) -> [String] Source # isVariable :: Ambiguous (Term ext) -> Bool Source # isConstant :: Ambiguous (Term ext) -> Bool Source # isAtomary :: Ambiguous (Term ext) -> Bool Source # size :: Ambiguous (Term ext) -> Int Source #
HasVariables ext => HasVariables (Term ext) Source #
Methods variables :: Term ext -> [String] Source # isVariable :: Term ext -> Bool Source # isConstant :: Term ext -> Bool Source # isAtomary :: Term ext -> Bool Source # size :: Term ext -> Int Source #
HasVariables term => HasVariables (Marked term) Source #
Methods variables :: Marked term -> [String] Source # isVariable :: Marked term -> Bool Source # isConstant :: Marked term -> Bool Source # isAtomary :: Marked term -> Bool Source # size :: Marked term -> Int Source #
HasVariables ext => HasVariables (Formula ext) Source #
Methods variables :: Formula ext -> [String] Source # isVariable :: Formula ext -> Bool Source # isConstant :: Formula ext -> Bool Source # isAtomary :: Formula ext -> Bool Source # size :: Formula ext -> Int Source #