package provers
Content Hierarchy
Ordering
- Alphabetic
Visibility
- Public
- Protected
Package Members
Type Members
- trait IncrementalProver extends Prover
A prover that determines validity via an incremental proof session.
- trait OneShotProver extends Prover
A prover that interprets Sessions as stack operations.
- trait Prover extends AnyRef
A prover that is able to refute HOL sequents/formulas (or subsets of HOL, like propositional logic).
A prover that is able to refute HOL sequents/formulas (or subsets of HOL, like propositional logic).
TODO: exceptions to indicate that a formula is not supported (e.g. for propositional provers).
Implementors may want to override isValid(seq) to avoid parsing proofs.
- trait ResolutionProver extends OneShotProver
Value Members
- object Session
Implementation of proof sessions via the cats free monad.
Implementation of proof sessions via the cats free monad. See http://typelevel.org/cats/datatypes/freemonad.html.
- object extractIntroducedDefinitions
- object groundFreeVariables
- object mangleName
- object renameConstantsToFi
This is the API documentation for GAPT.
The main package is gapt.