moltap Contents Index

Moltap.Prover.TableauState Portability portable Stability experimental Maintainer twanvl@gmail.com

Contents Tableau and state types Functions on the state Navigating the tree Adding formulas Testing for axioms Extracting results

Description

The state type for tableau computations.

Synopsis

module Moltap.Prover.SplitStateMonad data GenTableau p e = Tableau { tabSeen :: (Map Formula p) tabUniversal :: [(Agents, GenTableauM_ p e)] } data GenTableauState p e = TableauState { tabZipper :: (GenTableauTree p e) tabAxioms :: Axioms } emptyTableauState :: Axioms -> GenTableauState p e type GenTableauM p e a = SSM (GenTableauState p e) e a type GenTableauM_ p e = GenTableauM p e () tabLocalDown :: (Show p, Monoid e) => Agents -> GenTableauM_ p e -> GenTableauM_ p e tabLocalUpIf :: Monoid e => (AxiomSet -> Bool) -> Agents -> GenTableauM_ p e -> GenTableauM_ p e -> GenTableauM_ p e tabAddUniv :: Monoid e => Agents -> GenTableauM_ p e -> GenTableauM_ p e tabMemo :: (Formula -> p -> p -> GenTableauM p e a) -> (Formula -> p -> GenTableauM p e a) -> Formula -> p -> GenTableauM p e a tabWrapIfAxiom :: (AxiomSet -> Bool) -> Agents -> (GenTableauM_ p e -> GenTableauM_ p e) -> GenTableauM_ p e -> GenTableauM_ p e tabWhenAxiom :: (AxiomSet -> Bool) -> Agents -> GenTableauM_ p e -> GenTableauM_ p e tabGraph :: GenTableauState p e -> [(Int, GenTableau p e, [(Int, Agents)])]

Documentation

module Moltap.Prover.SplitStateMonad

Tableau and state types

data GenTableau p e

A tableau for a single world Constructors Tableau tabSeen :: (Map Formula p) Things we have already seen tabUniversal :: [(Agents, GenTableauM_ p e)] Things that hold in all reachable worlds Instances ??? e p => Show (GenTableau p e)

data GenTableauState p e

State in a tableau computation, generalized over proof type. Constructors TableauState tabZipper :: (GenTableauTree p e) The tableaux for the current world tabAxioms :: Axioms Axioms that hold for different agents Instances ??? e p => Show (GenTableauState p e)

emptyTableauState :: Axioms -> GenTableauState p e

The initial tableau state

type GenTableauM p e a = SSM (GenTableauState p e) e a

type GenTableauM_ p e = GenTableauM p e ()

Functions on the state

Navigating the tree

tabLocalDown :: (Show p, Monoid e) => Agents -> GenTableauM_ p e -> GenTableauM_ p e

Perform a tableau computation in a new world reachable from the current one by the given agents.

tabLocalUpIf

:: Monoid e => (AxiomSet -> Bool) required axioms -> Agents agents to match -> GenTableauM_ p e action to perform locally -> GenTableauM_ p e action to perform otherwise -> GenTableauM_ p e Perform a tableau computation in a world from which the current one is reachable, and it is reached by an agent matching the test.

Adding formulas

tabAddUniv :: Monoid e => Agents -> GenTableauM_ p e -> GenTableauM_ p e

Add a universal, instantiate it for matching worlds

tabMemo

:: (Formula -> p -> p -> GenTableauM p e a) The formula was already processed before -> (Formula -> p -> GenTableauM p e a) The formula was not processed before -> Formula -> p Formula and proof -> GenTableauM p e a Memoize a formula. If the formula was already seen perform old to merge the possible conflict. Otherwise memoize it and perform new.

Testing for axioms

tabWrapIfAxiom :: (AxiomSet -> Bool) -> Agents -> (GenTableauM_ p e -> GenTableauM_ p e) -> GenTableauM_ p e -> GenTableauM_ p e

If an axiom holds, wrap a, else don't change anything

tabWhenAxiom :: (AxiomSet -> Bool) -> Agents -> GenTableauM_ p e -> GenTableauM_ p e

If an axiom holds, perform an axiom, otherwise do nothing

Extracting results

tabGraph :: GenTableauState p e -> [(Int, GenTableau p e, [(Int, Agents)])]

Convert the tableau state to a graph of tableaux

Produced by Haddock version 0.8