Zsyntax

Documentation

module Zsyntax.Formula

search :: Ord a => Sequent a -> (SearchRes (DecoratedLSequent a Label), [DecoratedLSequent a Label])

Searches for a derivation of the specified sequent.

search g == searchLabelled (toLabelledGoal g)

searchLabelled :: Ord a => GoalNSequent a Label -> (SearchRes (DecoratedLSequent a Label), [DecoratedLSequent a Label])

Searches for a derivation of the specified goal sequent. Returns the search results, as well as all searched sequents.

toLabelledGoal :: Ord a => Sequent a -> GoalNSequent a Label

Turns a sequent into a labelled sequent that is suitable for proof search, by breaking the linear context formulas into neutral formulas, and labelling all subformulas with unique labels.

type SearchRes a = [Res a]

Type representing the result of proof search. Every element in the list corresponds to the result of analysing node in the search space by the search algorithm. The result is Res in the positive case the node is a goal node, or Delay in the negative case.

The search agorithm produces an element of `SearchRes a` lazily, inserting Delay constructors to ensure that the computation is productive even in the case no goal node is found in the search space. This allows to perform proof search in an on-demand fashion, possibly giving up after a certain number of Delays.

data Extraction a

Type of the result of extractResults, which extracts all positive search results from a search result stream. An element of `Extraction a` is either a non-empty list of positive results, or an element of SpaceExhausted giving a reason why no result was found.

Constructors

AllResults (NonEmpty a)

NoResults FailureReason

data FailureReason

Type of reasons why no result can be extracted from a search result stream.

Either the search space has been exhaustively searched and no result was found (the query is not a theorem), or the search was terminated preemptively according to an upper bound imposed on the maximum depth of the search space.

Constructors

NotATheorem

SpaceTooBig

type DecoratedLSequent a l = DerivationTerm a l ::: LSequent a l

type Label = Int

extractResults :: Int -> SearchRes a -> Extraction a

Extract all the positive results from a search result stream, stopping if no result is found after the given number of delays.