gapt
2.18.0-SNAPSHOT
gapt
API
gapt
cli
CLIMain
ScriptsResultHolder
GPL
GaptRepl
GaptReplDriver
GaptTerminal
GaptScriptInterpreter
cutintro
ClauseWithIndexLists
ClausesWithIndexLists
CutIntroduction
BackgroundTheory
Equality
prover
PureFOL
prover
BackgroundTheory
CutIntroException
InputProof
InputProof
NonCoveringGrammarException
UnprovableException
computeSolutionViaDls
GrammarFindingMethod
LeafIndex
LiteralWithIndexLists
MaxSATMethod
MaxSATMethod
Pi2CutIntroduction
Pi2SeHs
ReforestMethod
SchematicExtendedHerbrandSequent
SolutionStructure
beautifySolution
gStarUnify
improveSolutionLK
introducePi2Cut
pi2GrammarToSEHS
proveWithPi2Cut
sehsToVTRATG
solutionViaInterpolation
vtratgToSEHS
doc
Chunk
CliListing
CommandEvaluator
Document
ResultHolder
Section
TacticsListing
Text
WriterOutputStream
evalCodeSnippets
evaluate
parse
Parser
examples
church_numerals
cond
int_of_num
is_num
num
plus
times
hoare
addition
array_init
induction
associativity
associativitySpecialCase
comm
evenodd
factorial
primeFactor
nd
AndLeftWithEmptySuccedent
OrLeftWithEmptySuccedent
classicalPairing
contractRightWithWrongFocus
cut1
cut2
definitionLeftRule
definitionRightRule
definitionRightRule2
demorgan1
demorgan2
dne
equalityLeft
equalityLeftEmptySuc
equalityRight
ex0_1_6
ex0_1_6_short
example1
impLeft1
impLeft2
impRight1
impRight2
induction
inductionRule
issue687
issue688
lem
negLeft
negLeftFollowedByNegRight
negLeftRight1
negRight1
orLeft1
orLeft2
orLeft3
orLeft4
orLeft5
orRight1
orRight2
proofLink
proofLink2
proofLink3
weakenContractRight1
weakeningRight
weakeningRight1
weakeningRight2
weakeningRightWithWrongFocus
poset
cutintro
proof
prime
PrimeDefinitions
euclid
euclid3
furstenberg
furstenberg3
furstenbergWitness
Multiset
ZZMPolynomial
ZZMPolynomial
recschem
vtrat_comparison
sequence
AllQuantifiedConditionalAxiomHelper
ExplicitEqualityTactics
FactorialFunctionEqualityExampleProof
FactorialFunctionEqualityExampleProof2
LinearCutExampleProof
LinearEqExampleProof
LinearExampleProof
LinearRightCutExampleProof
ProofSequence
SquareDiagonalExampleProof
SquareEdges2DimExampleProof
SquareEdgesExampleProof
SumExampleProof
SumOfOnesExampleProof
SumOfOnesF2ExampleProof
SumOfOnesFExampleProof
UniformAssociativity3ExampleProof
theories
Theory
DelayedProofResult
DelayedProofResult
Theory
LemmaHandle
LemmaHandle
Theory0
fta
list
listdrop
listfold
listlength
logic
nat
natdivisible
natdivision
natlists
natorder
props
set
tip
grammars
simp_expr_unambig1
isaplanner
prop_03
prop_06
prop_07
prop_08
prop_09
prop_10
prop_11
prop_12
prop_13
prop_14
prop_15
prop_16
prop_17
prop_18
prop_19
prop_21
prop_22
prop_23
prop_24
prop_26
prop_27
prop_28
prop_29
prop_30
prop_31
prop_32
prop_33
prop_34
prop_35
prop_36
prop_37
prop_38
prop_39
prop_40
prop_41
prop_42
prop_43
prop_44
prop_45
prop_46
prop_47
prop_48
prop_49
prop_59
prod
prop_01
prop_04
prop_05
prop_06
prop_07
prop_08
prop_10
prop_13
prop_15
prop_16
prop_20
prop_27
prop_28
prop_29
prop_30
prop_31
prop_32
prop_33
prop_34
prop_35
BussTautology
CASCData
CASCEvaluation
CERESExpansionExampleProof
CountingEquivalence
ECSJumpSchema
EventuallyConstantSchema
EventuallyConstantSchemaInductionRefutation
EventuallyConstantSchemaRefutation
ExponentialCompression
FirstSchema0
FirstSchema1
FirstSchema2
FirstSchema3
FirstSchema4
FirstSchema5
FirstSchema6
FirstSchema7
FirstSchema8
FirstSchema9
Formulas
Peano
FourStrictMonotoneSchema
FunctionIterationRefutation
FunctionIterationRefutationPos
FunctionIterationSchema
GradedStrictMonotoneSchema
GradedStrictMonotoneSequenceRefutation
GradedStrictMonotoneSequenceSchema
MonoidCancellation
NdiffSchema
NiaSchema
NiaSchemaRefutation
OneStrictMonotoneRefutation
OneStrictMonotoneSchema
OneStrictMonotoneSequenceRefutation
OneStrictMonotoneSequenceSchema
PQPairs
Permutations
Pi2Pigeonhole
Pi3Pigeonhole
PigeonHolePrinciple
ReductionDemo
ReforestDemo
Script
SimpleMutualInductionSchema
StrictMonotoneSchema
StrongStrictMonotoneSchema
ThreeStrictMonotoneRefutation
ThreeStrictMonotoneSchema
TwoStrictMonotoneRefutation
TwoStrictMonotoneSchema
VeryWeakLexicoPHPSchema
VeryWeakLexicoPHPSchemaVariant
VeryWeakLexicoPHPSchemaVariantRefutation
VeryWeakPHPSeqSchema
VeryWeakPHPSeqTwoSchema
VeryWeakPHPSequenceVariantSchema
divisionByTwo
drinker
elemAtIndex
epsilon
fol1
fol2
gapticExamples
gniaSchema
implicationLeftMacro
instprover
lattice
nTape2
nTape2
nTape3
nTape3
nTape4
nTape4
nTape5
nTape5
nTape5Arith
nTape5Arith
nTape6
formulas
sequents
nTapeInstances
philsci
primediv
successor
tape
tapeUrban
tautSchema
tbillc
expr
formula
constants
AndC
BottomC
EqC
ExistsC
ForallC
ImpC
LogicalC
LogicalConstant
MonomorphicLogicalC
NegC
OrC
QuantifierC
TopC
fol
BinaryConnective
FOLAtom
FOLAtom
FOLAtomConst
FOLAtomConst
FOLConst
FOLConst
FOLExpression
FOLFormula
FOLFunction
FOLFunctionArgs
FOLFunctionConst
FOLFunctionConst
FOLFunctionName
FOLHeadType
FOLPartialAtom
FOLPartialTerm
FOLPosition
FOLPosition
FOLQuantifier
FOLTerm
FOLVar
FOLVar
Hol2FolDefinitions
Numeral
QuantifierStructure
Exists
Forall
Utils
changeTypeIn
flatSubterms
folTermSize
getArityOfConstants
invertBijectiveMap
isFOLFunction
isFOLPrenexPi1
isFOLPrenexSigma1
isPrenexPi1
isPrenexSigma1
naive
atMost
exactly
natMaker
reduceHolToFol
replaceAbstractions
thresholds
atMost
exactly
undoHol2Fol
undoReplaceAbstractions
hol
BinaryConnective
HOLAtomConst
HOLAtomConst
HOLFunction
HOLOrdering
HOLOrdering
HOLPartialAtom
HOLPosition
HOLPosition
TAOrdering
TAOrdering
atoms
containsHOQuantifier
containsQuantifier
containsQuantifierOnLogicalLevel
containsStrongQuantifier
containsWeakQuantifier
dualize
existentialClosure
formulaToSequent
freeHOVariables
inductionPrinciple
instantiate
isAtom
isExtendedAtom
isLogicalConstant
isNeg
isPrenex
isReflexivity
lcomp
normalizeFreeVariables
numOfAtoms
removeAllQuantifiers
removeNeg
universalClosure
prop
PropAtom
PropAtom
PropConnective
PropFormula
All
And
Atom
Atom
BinaryPropConnectiveHelper
Bottom
Eq
Ex
Formula
Iff
Imp
Block
MonoidalBinaryPropConnectiveHelper
nAry
Neg
NonLogicalConstant
NullaryPropConnectiveHelper
Or
Quant
QuantifierHelper
Block
Top
UnaryPropConnectiveHelper
subst
ExprSubstWithβ
ExprSubstWithβ0
ExprSubstWithβ1
ExprSubstitutable1
SubstitutableTy
ExprSubstitutable2
ExprSubstitutable3
ExprSubstitutable4
ExprSubstitutable5
ExprSubstitutable6
ExprSubstitutable7
FOLSubstitution
FOLSubstitution
PreSubstitution
PreSubstitution
SeqSubstitutable
Substitutable
Substitutable
Substitution
Substitution
ty
->:
FunctionType
TArr
TBase
TBase
TVar
Ti
To
Ty
arity
baseTypes
util
ConditionalNormalizer
ConditionalReductionRule
ConditionalReductionRule
ExpressionParseHelper
ExpressionSplice
IdentifierSplice
Splice
ExpressionParseHelper
LambdaPosition
Choice
Left
Right
LambdaPosition
boundVariables
constants
nonLogical
expressionDepth
expressionSize
freeVariables
isConstructorForm
isGround
isInVNF
longNormalForm
rename
replacementContext
subTerms
syntacticMGU
syntacticMatching
toVNF
typeVariables
variables
Abs
Abs
Block
App
App
Apps
BetaReduction
Const
Const
Expr
ExprNameGenerator
Normalizer
Normalizer
ReductionRule
ReductionRule
Replaceable
Replaceable
definitionReplaceable
holAtomReplaceable
substitutionReplaceable
unitReplaceable
ReplaceableInstances0
exprReplaceable
structReplaceable
ReplaceableInstances1
formulaReplaceable
ReplaceableInstances2
TermReplacement
Var
Var
VarOrConst
VarOrConst
containedNames
normalize
preExpr
Abs
App
ArrType
BaseType
ElabError
ElabError
Expr
FlatOps
Ident
LocAnnotation
Location
MetaType
MetaTypeIdx
Mismatch
OccursCheck
Quoted
ReadablePrinter
Type
TypeAnnotation
UnificationError
VarType
formats
babel
BabelElabError
BabelExporter
Bare
IdentShowMode
Parenable
Safe
WithParams
WithType
BabelLexical
BabelParseError
BabelParser
BabelParserCombinators
BabelParsingError
BabelSignature
BabelSignature
IsConst
IsUnknownConst
IsVar
VarConst
defaultSignature
MapBabelSignature
MapBabelSignature
Notation
Notation
Alias
ConstName
ConstName
IffName
Infix
Infix
NeqName
Postfix
Prefix
Quantifier
RealConst
Token
Token
Notations
Notations
Precedence
csv
CSVConvertible
CSVFile
CSVFile
CSVRow
dimacs
DIMACS
DIMACSEncoding
readDIMACS
readDRUP
readWDIMACS
writeDIMACS
writeWDIMACS
hoare
ProgramParser
ProgramParserA
ivy
conversion
IvyToResolution
Flip
InitialClause
Instantiate
IvyParser
IvyResolutionProof
NewSymbol
Paramodulation
Propositional
Resolution
json
et
ExpansionTreeCodec
lk
LKProofCodec
nd
NDProofCodec
ExprCodec
JsonExporter
JsonImporter
JsonToDoc
SequentCodec
latex
LatexExporter
SequentsListLatexExporter
leancop
LeanCoP21Parser
Clause
Hash
Lit
Neg
NegHash
Pos
Proof
LeanCoPLeanPredWrongArityException
LeanCoPNoLeanPredException
LeanCoPNoMatchException
LeanCoPParser
Clause
FOLLiteral
InputFormula
LeanCoPParserException
lisp
LAtom
LCons
LFun
LFunOrAtom
LKeyword
LList
LList
LSymbol
LSymbol
SExpression
SExpressionParser
llk
ast
Abs
All
And
App
Bottom
Eq
Exists
Imp
LambdaAST
Neg
Or
Top
Var
short
hof
hot
sig
AToken
DeclarationParser
DeclarationParser
EquationVerifier
Different
Equal
EqualModuloEquality
ReplacementResult
ExtendedProofDatabase
HybridLatexParserException
LLKASTParser
LLKASTParser
LLKExporter
LLKExporter
LLKFormatter
LLKFormulaParser
LLKFormulaParser
LLKProofParser
LLKProofParser
LLKTypes
LatexLLKExporter
LatexReplacementParser
RToken
TToken
Token
TokenToLKConverter
UnicodeToLatex
exportLLK
loadLLK
parseLLKExp
parseLLKFormula
toLLKString
toLatexString
prover9
Prover9TermParser
Prover9TermParserA
Prover9TermParserLadrStyle
smt
SmtLibExporter
tip
analysis
SymbolTable
Type
retrieveDatatypes
compiler
TipSmtToTipProblemCompiler
TipTransformationCompiler
decoration
ReconstructDatatypes
export.export
parser
Datatype
TipSmtAnd
TipSmtAssertion
TipSmtAst
TipSmtCase
TipSmtCheckSat
TipSmtCommand
TipSmtConstantDeclaration
TipSmtConstructor
TipSmtConstructorField
TipSmtConstructorPattern
TipSmtDatatype
TipSmtDatatypesDeclaration
TipSmtDefault
TipSmtDefinitionVisitor
TipSmtDistinct
TipSmtEq
TipSmtExists
TipSmtExpression
TipSmtFalse
TipSmtForall
TipSmtFormalParameter
TipSmtFun
TipSmtFunctionDeclaration
TipSmtFunctionDefinition
TipSmtGoal
TipSmtIdentifier
TipSmtImp
TipSmtIte
TipSmtKeyword
TipSmtMatch
TipSmtMutualRecursiveFunctionDefinition
TipSmtNot
TipSmtOr
TipSmtParser
TipSmtParserException
TipSmtPattern
TipSmtProblem
TipSmtSortDeclaration
TipSmtTrue
TipSmtType
TipSmtVariableDecl
toSExpression
toTipAst
transformation
BooleanConstantElimination
DesugarDistinctExpression
EliminateUselessQuantifiers
ExpandConstructorMatch
IntegerToNaturalConversion
MoveUniversalQuantifiersInwardsTransformation
TipOcnf
TipSmtDefaultPatternExpansion
TipSmtDefinitionTransformation
TipSmtProblemTransformation
UseDefinitionEquations
VariableMatchExpansion
Exists
Forall
Polarity
desugarDistinctExpressions
eliminateBooleanConstants
eliminateRedundantQuantifiers
expandConstructorMatchExpressions
expandDefaultPatterns
expandVariableMatchExpressions
integersToNaturals
moveUniversalQuantifiersInwards
toOuterConditionalNormalForm
useDefiningFormulas
util
FreeVariablesProblem
Substitute
Substitution
TipNameGenerator
find
freeVariables
TipFun
TipProblem
TipProblemDefinition
TipSmtImporter
subterms
tipScalaEncoding
tptp
statistics
CASCResult
CASCResult
CommonProofStats
ErrorBags
ErrorBags
FileData
FileNotFound
MalformedFile
ParsingError
RPProofStats
RPProofStats
ReconstructionError
ReconstructionGaveUp
ReconstructionTimeout
ResultBundle
StackOverflow
TPTPstatistics
TptpInputStats
TptpLibraryProblem
TstpError
TstpError
TstpProofStats
TstpProofStats
TstpStatistics
UnknownFile
AnnotatedFormula
GeneralColon
GeneralList
IncludeDirective
MalformedInputFileException
TptpAxiom
TptpConjecture
TptpDefinition
TptpFOLExporter
TptpFile
TptpFormulaRole
TptpFormulaRoles
TptpHOLExporter
TptpHOLExporter
TptpImporter
TptpInput
TptpNegatedConjecture
TptpParser
TptpProblemToResolution
TptpProofParser
TptpTerm
TptpToString
resolutionToTptp
resolveIncludes
sequentProofToTptp
sequentProofToTptp
verit
alethe
AletheException
AletheParser
AletheProof
Anchor
Application
Argument
Assume
Exists
False
Forall
Identifier
Let
Not
Numeral
ProofCommand
Sort
SpecialConstant
Step
Term
True
VariableDeclaration
parseAletheProof
VeriTParser
VeriTParserException
VeriTUnfoldingTransitivityException
ClasspathInputFile
ClasspathInputFile
InputFile
InputFile
OnDiskInputFile
StdinInputFile
StdinInputFile
StringInputFile
implicits
grammars
reforest
Digram
Feature
Reforest
ReforestState
RigidTrigram
DeltaTableMethod
GeneralLeastGeneralGeneralization
InductionGrammar
InductionGrammar
Instantiation
Production
Production
checkable
isReplaceable
productionReplaceable
InductionGrammarMinimizationFormula
Pi2Grammar
Pi2Grammar
Pi2PreGrammar
RecSchemGenLangFormula
RecSchemTemplate
RecSchemTemplate
RecursionScheme
RecursionScheme
Rule
TRATG
TargetFilter
VTRATG
VTRATG
VectGrammarMinimizationFormula
VtratgParameter
VtratgParameter
VtratgTermGenerationFormula
canonicalVars
deltaTableAlgorithm
findMinimalInductionGrammar
findMinimalPi2Grammar
findMinimalVTRATG
instantiateRS
leastGeneralGeneralization
leastGeneralGeneralization
leastGeneralGeneralization1
minimizeInductionGrammar
minimizePi2Grammar
minimizeRecursionScheme
minimizeVTRATG
preOrderTraversal
qbupForRecSchem
recSchemIsReplaceable
recSchemToVTRATG
ruleIsReplaceable
rulesClosedUnderSubstitution
simplePi1RecSchemTempl
stableInductionGrammar
stablePi2Grammar
stableTerms
stableVTRATG
stsSubsumedByLGG
subsetLGGs
logic
bdt
BDT
BDT
F
Ite
T
fol
TseitinCNF
TseitinCNF
hol
dls
PredicateVariable
dls
simplify
vectorEq
AndOr
CNFn
CNFp
DNFn
DNFp
SkolemFunctions
SkolemFunctions
fastStructuralCNF
isOrevkovClass1
moveQuantifiers
removeRedundantQuantifiers
simplifyPropositional
skolemize
solveFormulaEquation
toNNF
AllDistinct
EqualityReflexivity
EqualityTransitivity
FunctionCongruence
Polarity
Polarity
PredicateCongruence
clauseSubsumption
toImplications
models
PropositionalModel
PropositionalModel
proofs
ceres
A
CERES
CERES
CLS
CharFormN
CharFormP
CharFormPRN
CharFormPRP
CharacteristicClauseSet
CharacteristicClauseSet
DeleteTautology
Dual
EmptyPlusJunction
EmptyTimesJunction
InstanceOfSchematicStruct
InstantiateStruct
Pickrule
Plus
PlusN
Projections
SchematicLeafs
SchematicStruct
SimplifyStruct
SingleProjection
SingleProjectionWithQuantifiers
Struct
StructCreators
StructTransformer
StructVisitor
Times
Times
Viperize
coloredStructString
deleteTautologies
extractStruct
simpleUnitResolutionNormalization
subsumedClausesRemoval
ceres_omega
AnalysisWithCeresOmega
StandardClauseSet
StandardClauseSet
context
facet
BaseTypes
BaseTypes
ConditionalReductions
ConditionalReductions
Constants
Constants
Definitions
Definitions
Facet
Facet
ProofDefinitions
ProofDefinitions
ProofNames
ProofNames
Reductions
Reductions
StructurallyInductiveTypes
StructurallyInductiveTypes
immutable
ImmutableContext
ImmutableContext
mutable
MutableContext
MutableContext
ReadOnlyMutableContext
WriteOnlyMutableContext
update
ConditionalReductionRuleUpdate
ConditionalReductionRuleUpdate
ConstantDeclaration
Definition
Definition
InductiveType
InductiveType
Constructor
Constructor
Field
InductiveTypeInternalParser
InductiveTypeLegacyParser
InductiveTypeParser
InductiveTypeValidator
InductiveTypeValidator
PrimitiveRecursiveFunction
PrimitiveRecursiveFunction
PrimitiveRecursiveFunctions
ProofDeclaration
ProofDefinitionDeclaration
ProofNameDeclaration
ReductionRuleUpdate
ReductionRuleUpdate
SkolemFunction
Sort
Sort
TypeDefinition
Update
Update
Context
Context
ProofDefinition
State
State
simplificationRules
epsilon
CriticalFormula
Epsilon
EpsilonC
EpsilonProof
ExpansionProofToEpsilon
epsilonize
expansion
BinaryExpansionTree
ETAnd
Flat
ETAtom
ETBottom
ETCut
Cut
Cut
ETDefinition
ETImp
ETInduction
Case
Induction
ETMerge
ETMerges
ETNeg
ETOr
ETSkolemQuantifier
ETStrongQuantifier
ETStrongQuantifierBlock
ETTop
ETWeakQuantifier
ETWeakQuantifierBlock
ETWeakening
ETt
ETt
closedUnderRepl
closedUnderSubst
ETtAtom
ETtBinary
ETtDef
ETtMerge
ETtMerge
ETtNullary
ETtPrettyPrinter
ETtSkolem
ETtStrong
ETtUnary
ETtWeak
ETtWeak
ETtWeakening
ExpansionProof
ExpansionProof
checkable
closedUnderRepl
closedUnderSubst
ExpansionProofToLK
withIntuitionisticHeuristics
ExpansionProofToLK
Theory
ExpansionProofToMG3i
ExpansionProofToMG3i
ExpansionProofToMG3iViaSAT
ExpansionProofToMG3iViaSAT
ExpansionTree
ExpansionTree
checkable
closedUnderReplacement
ExpansionTreePrettyPrinter
InstanceTermEncoding
InstanceTermEncoding
PropositionalExpansionProofToLK
RichExpansionSequent
addSymmetry
atomicExpansionET
cleanStructureET
commuteReplacementCtxWithDefEq
deskolemizeET
eigenVariablesET
eliminateCutsET
eliminateDefsET
DefinitionFormula
eliminateMerges
extractInstances
findMerges
formulaToExpansionTree
freeVariablesET
generalizeET
groundTerms
insertDefinition
instReplCtx
isPropositionalET
minimalExpansionSequent
minimalExpansionSequents
moveDefsUpward
moveSkolemNodesToCuts
nonProofTheoreticSkolemTerms
numberOfInstancesET
prenexifyET
pushWeakeningsUp
removeSkolemCongruences
replaceAtHOLPosition
replaceWithContext
tautAtomicExpansionET
unifyInstancesET
gaptic
tactics
AnalyticInductionTactic
AnalyticInductionTactic
AndLeftTactic
AndRightTactic
BottomAxiomTactic
ChainTactic
CutTactic
EqualityTactic
ExistsLeftTactic
ExistsRightTactic
FocusTactic
ForallLeftTactic
ForallRightTactic
ForwardChain
ImpLeftTactic
ImpRightTactic
InductionTactic
InsertTactic
LogicalAxiomTactic
NegLeftTactic
NegRightTactic
OrLeftTactic
OrRightTactic
ProofLinkTactic
PropTactic
QuasiPropTactic
ReflexivityAxiomTactic
Refl
RenameTactic
RepeatTactic
ReplaceTactic
ResolutionProverTactic
RewriteTactic
StrongQuantTactic
SubstTactic
SuperpositionInductionTactic
TopAxiomTactic
UnfoldTactic
UnfoldTacticHelper
WeakeningLeftTactic
WeakeningRightTactic
AnyFormula
BinaryTactic
CanLabelledSequent
CanLabelledSequent
IncompleteProof
Helper
Lemma
Helper
LemmaHelper
LemmaMacros
NewLabel
NewLabels
OnLabel
OpenAssumption
OpenAssumptionIndex
Proof
Helper
ProofState
ProofState
ProofSegmentInsertionVisitor
QedFailureException
SimpleLemmaHelper
Tactic
Tactic
TacticApplyMode
TacticBlockArgument
TacticCommands
TacticCommands
currentGoal
TacticEitherOps
TacticFailure
TacticFailure
TacticFailureException
TacticFailureFailureException
TacticMonad
TacticOptionOps
Tactical
Tactical1
FindFormula
TacticsProof
TacticsProof0
UniqueFormula
guessLabels
hoare
Assign
Assign
Blocks
ForLoop
ForLoop
IfElse
LoopFree
Program
Sequence
Sequence
SimpleInductionProblem
SimpleLoopProblem
Skip
mapVariableNames
substVariables
unrollLoop
usedVariables
weakestPrecondition
lk
reductions
CutReduction
GradeReductionAnd
GradeReductionAxiomBottom
GradeReductionAxiomLeft
GradeReductionAxiomRight
GradeReductionAxiomTop
GradeReductionDefinition
GradeReductionEquality
GradeReductionExists
GradeReductionForall
GradeReductionImp
GradeReductionNeg
GradeReductionOr
GradeReductionWeakeningLeft
GradeReductionWeakeningRight
InductionUnfoldingReduction
LeftRankAndLeftReduction
LeftRankAndRightReduction
LeftRankContractionLeftReduction
LeftRankContractionRightReduction
LeftRankCutReduction
LeftRankDefinitionLeftReduction
LeftRankDefinitionRightReduction
LeftRankEqualityLeftReduction
LeftRankEqualityRightReduction
LeftRankExistsLeftReduction
LeftRankExistsRightReduction
LeftRankExistsSkLeftReduction
LeftRankForallLeftReduction
LeftRankForallRightReduction
LeftRankForallSkRightReduction
LeftRankImpLeftReduction
LeftRankImpRightReduction
LeftRankInductionReduction
LeftRankNegLeftReduction
LeftRankNegRightReduction
LeftRankOrLeftReduction
LeftRankOrRightReduction
LeftRankWeakeningLeftReduction
LeftRankWeakeningRightReduction
MaximumGradeSelector
MaxGradeReduction
NonPropositionalCutFilter
RedexFilter
Reduction
RightRankAndLeftReduction
RightRankAndRightReduction
RightRankContractionLeftReduction
RightRankContractionRightReduction
RightRankCutReduction
RightRankDefinitionLeftReduction
RightRankDefinitionRightReduction
RightRankEqualityLeftReduction
RightRankEqualityRightReduction
RightRankExistsLeftReduction
RightRankExistsRightReduction
RightRankExistsSkLeftReduction
RightRankForallLeftReduction
RightRankForallRightReduction
RightRankForallSkRightReduction
RightRankImpLeftReduction
RightRankImpRightReduction
RightRankInductionReduction
RightRankNegLeftReduction
RightRankNegRightReduction
RightRankOrLeftReduction
RightRankOrRightReduction
RightRankWeakeningLeftReduction
RightRankWeakeningRightReduction
UppermostRedexFilter
gradeReduction
leftRankReduction
maximumGrade
rightRankReduction
rules
macros
AndLeftMacroRule
ContractionLeftMacroRule
ContractionMacroRule
ContractionRightMacroRule
EqualityLeftMacroRule
EqualityRightMacroRule
ExchangeLeftMacroRule
ExchangeRightMacroRule
ExistsLeftBlock
ExistsRightBlock
FOTheoryMacroRule
ForallLeftBlock
ForallRightBlock
ImpRightMacroRule
NaturalNumberInductionRule
OrRightMacroRule
ParamodulationLeftRule
ParamodulationRightRule
TransRule
WeakQuantifierBlock
WeakeningContractionMacroRule
WeakeningLeftMacroRule
WeakeningMacroRule
WeakeningRightMacroRule
proofFromInstances
AndLeftRule
AndLeftRule
AndRightRule
AndRightRule
BinaryLKProof
BinaryLKProof
BottomAxiom
CommonRule
ContractionLeftRule
ContractionLeftRule
ContractionRightRule
ContractionRightRule
ContractionRule
ConvenienceConstructor
ConversionLeftRule
ConversionLeftRule
ConversionRightRule
ConversionRightRule
ConversionRule
ConversionRule
CutRule
CutRule
Eigenvariable
EqualityLeftRule
EqualityLeftRule
EqualityRightRule
EqualityRightRule
EqualityRule
EqualityRule
ExistsLeftRule
ExistsLeftRule
ExistsRightRule
ExistsRightRule
ExistsSkLeftRule
ExistsSkLeftRule
ForallLeftRule
ForallLeftRule
ForallRightRule
ForallRightRule
ForallSkRightRule
ForallSkRightRule
ImpLeftRule
ImpLeftRule
ImpRightRule
ImpRightRule
InductionCase
InductionRule
InitialSequent
InitialSequent
LogicalAxiom
NegLeftRule
NegLeftRule
NegRightRule
NegRightRule
OrLeftRule
OrLeftRule
OrRightRule
OrRightRule
ProofLink
ProofLink
ReflexivityAxiom
SkolemQuantifierRule
StrongQuantifierRule
StrongQuantifierRule
TopAxiom
UnaryLKProof
UnaryLKProof
WeakQuantifierRule
WeakQuantifierRule
WeakeningLeftRule
WeakeningRightRule
transformations
IterativeParallelStrategy
IterativeSelectiveStrategy
LKToExpansionProof
LKToND
LKToNDTranslationException
LeftRankInductionUnfoldingReduction
LowerMostRedexReducer
MG3iToLJ
ParallelAtDepthStrategy
RedexReducer
ReductionStrategy
ReductiveCutNormalization
emptyCutReduction
Selector
StuckCutReduction
Left
Right
UnfoldInductions
UppermostFirstStrategy
acnf
acnfTop
cleanCuts
cleanStructuralRules
cutNormal
eliminateDefinitions
eliminateDefinitions
equalityLeftReduction
equalityRightReduction
folSkolemize
inductionNormalForm
introOrCut
isAcnf
isAcnfTop
isAtomicCut
makeInductionExplicit
makeTheoryAxiomsExplicit
moveStrongQuantifierRulesDown
pushAllWeakeningsToLeaves
pushEqualityInferencesToLeaves
pushEqualityInferencesToLeaves2
pushSingleWeakeningToLeaves
skolemizeLK
unfoldInduction
unfoldInduction
weakeningOnlySubTree
util
ArithmeticInductionToSchema
AtomicExpansion
CreateASchemaVersion
EigenVariablesLK
EquationalLKProver
ExtractInterpolant
Interpolate
InterpolationException
IsKSimple
LKProver
SolveUtils
consoleString
containsDefinitionRules
containsEqualityReasoning
cutFormulas
cutsNumber
extractInductionAxioms
extractInductionGrammar
extractRecSchem
freeVariablesLK
groundFreeVarsLK
inductionEigenvariables
inductionsNumber
instanceProof
instantiateProof
isCutFree
isInductionFree
isMaeharaMG3i
isRegular
logicalComplexity
printProofStats
quantRulesNumber
regularize
rulesNumber
solvePropositional
solvePropositional
solveQuasiPropositional
strongQuantRulesNumber
weakQuantRulesNumber
Attributes
Attributes
AddAttributeUpdate
LKProof
LKProofReplacer
LKProofSubstitutable
LKProofSubstitutableDefault
LKRuleCreationException
LKVisitor
lkProofReplaceable
normalizeLKt
lkt
ALCtx
AllL
AllL
AllLBlock
AllR
AllR
AllRBlock
AllSk
AllSk
AndL
AndL
AndR
AndR
Ax
B1
B2
BN
BinConn
Bound
Bound1
Bound2
BoundN
Cut
Cut
Def
Def
Eql
Eql
FakeLocalCtx
FakeLocalCtx
FreshHyp
Hyp
Hyp
HypSet
ImplicitInstances
replaceable
replaceableBnd1
replaceableBnd2
replaceableBndN
replaceableIndCase
Ind
IndCase
LKToLKt
LKToLKt
LKt
TreeLikeOps
LKtToLK
Link
LocalCtx
LocalCtx
NegL
NegL
NegR
NegR
NoopSimpAdapter
Normalizer
ProofSubst
NormalizerWithDebugging
Rfl
SimpAdapter
SimplifierSimpAdapter
TopR
atomizeEquality
check
makeEqualityExplicit
makeEqualityExplicit
normalize
normalize
unfoldInduction
unfoldInduction
nd
AndElim1Rule
AndElim2Rule
AndIntroRule
BinaryNDProof
BinaryNDProof
BottomElimRule
CommonRule
ContractionRule
ContractionRule
ConvenienceConstructor
DefinitionRule
Eigenvariable
EqualityElimRule
EqualityElimRule
EqualityIntroRule
ExcludedMiddleRule
ExistsElimRule
ExistsElimRule
ExistsIntroRule
ExistsIntroRule
ForallElimBlock
ForallElimRule
ForallIntroRule
ForallIntroRule
ImpElimRule
ImpIntroRule
ImpIntroRule
InductionCase
InductionRule
InitialSequent
InitialSequent
LogicalAxiom
LogicalAxiom
MRealizability
NDProof
NDRuleCreationException
NegElimRule
NegIntroRule
NegIntroRule
OrElimRule
OrElimRule
OrIntro1Rule
OrIntro2Rule
TernaryNDProof
TernaryNDProof
TheoryAxiom
TopIntroRule
UnaryNDProof
UnaryNDProof
WeakeningRule
WeakeningRule
casesReplaceable
freeVariablesND
friedman
kolmogorov
replaceable
reduction
CNFReductionExpRes
CNFReductionLKRes
CNFReductionResRes
CNFReductionSequentsResRes
CombinedReduction
ErasureReductionCNF
ErasureReductionET
GroundingReductionET
HOFunctionReduction
HOFunctionReductionCNFRes
HOFunctionReductionET
HOFunctionReductionRes
LambdaEliminationReduction
LambdaEliminationReductionCNFRes
LambdaEliminationReductionET
LambdaEliminationReductionRes
OneWayReduction_
PredicateReductionCNF
PredicateReductionET
PredicateTranslation
Reduction
Reduction_
TagReductionCNF
TagReductionET
guessContext
resolution
AllL
AllL
AllR
AllR
Block
AndL
AndR1
AndR2
AvatarComponent
AvatarContradiction
AvatarDefinition
AvatarGeneralNonGroundComp
AvatarGroundComp
AvatarNegNonGroundComp
AvatarNonGroundComp
AvatarNonGroundComp
DefinitionFormula
AvatarSplit
AvatarSplit
BottomR
Clausifier
DefIntro
Defn
ExL
ExR
ExR
ExpansionToResolutionProof
Factor
Factor
Block
Flip
Flip
ImpL1
ImpL2
ImpR
InitialClause
Input
LocalResolutionRule
MguFactor
MguResolution
NegL
NegR
OrL1
OrL2
OrR
PCNF
Paramod
Paramod
PropositionalResolutionRule
Refl
Resolution
Resolution
Resolution2RalWithAbstractions
Resolution2RalWithAbstractions
ResolutionProof
ResolutionProofVisitor
ResolutionToExpansionProof
ResolutionToLKProof
ResolutionToRal
ResolutionToRal
SkolemQuantResolutionRule
SkolemQuantResolutionRuleCompanion
Subst
Subst
Taut
TopL
UnitResolutionToLKProof
WeakQuantResolutionRule
avatarComponentsAreReplaceable
containsEquationalReasoning
eliminateSplitting
expansionProofFromInstances
findDerivationViaResolution
fixDerivation
forgetfulPropParam
forgetfulPropResolve
mapInputClauses
numberOfLogicalInferencesRes
resolutionProofsAreReplaceable
simplifyResolutionProof
structuralCNF
tautologifyInitialUnitClauses
rup
Res
Res
Input
Resolve
Resolve
Taut
RupProof
RupProof
Delete
Delete
Input
Input
Line
Rup
Rup
sketch
RefutationSketch
RefutationSketchToResolution
SketchAxiom
SketchComponentElim
SketchComponentIntro
SketchInference
SketchSplitCombine
UnprovableSketchInference
Ant
Checkable
Checkable
ExpressionChecker
contextElementIsCheckable
expressionIsCheckable
lkIsCheckable
resolutionIsCheckable
typeIsCheckable
ContextRule
ContextSection
DagProof
DagProof
DagLikeOps
TreeLikeOps
IndexOrFormula
IndexOrFormula
IsFormula
IsIndex
NDSequent
NDSequent
ProofBuilder
ProofBuilder
RichClause
RichFOLSequent
RichFormulaSequent
SeqWrapper
Sequent
Sequent
SequentConnector
SequentConnector
SequentFlatMapOp
SequentFlattenOp
SequentIndex
SequentIndex
SequentProof
SetSequent
Suc
guessPermutation
loadExpansionProof
withSection
prooftool
AboveLinePanel
AlignmentChanged
CedentPanel
CollapsedSubproofsPanel
CommaLabel
ContainsLKProof
ContainsSequentProof
DagProofViewer
DrawETNonQuantifier
DrawETQuantifierBlock
DrawExpansionSequent
DrawExpansionTree
DrawExpansionTree
DrawList
DrawSequent
DrawSequent
DrawSequentInProof
DrawSequentProof
DrawSingleSequentInference
DrawStruct
ETQuantifierBlock
ETStrongQuantifierBlock
ExpansionSequentViewer
ExpansionTreeState
FileParser
FontChanged
HideDebugBorders
HideEndSequent
HideLeaf
HideProof
HideSequentContexts
HideSequentProof
HideStructuralRules
HideTree
LKProofViewer
LatexFormulaLabel
LatexIcon
LatexLabel
LatexLabel
LatexTurnstileLabel
ListViewer
MarkCutAncestors
MarkOccurrences
MenuButtons
NDProofViewer
NodeSelectedEvent
PTContentPanel
PTScrollPane
PopupMenu
PopupMenu
ProofColorizer
ProofLinePanel
ProofNode
ProofNodeInfo
ProofToolPublisher
ProofToolViewer
ProofWeighter
ProoflinkLabelPanel
ProoftoolViewable
ProoftoolViewable
RGBColorChooser
Rainbow
ReactiveSunburstModel
ReactiveSunburstView
Savable
ScrollableProofToolViewer
SequentProofViewer
ShowAllFormulas
ShowAllRules
ShowDebugBorders
ShowLeaf
ShowProof
ShowSequentProof
Spinner
StructViewer
SubproofsPanel
SunburstTreeDialog
TreeListPanel
NumLabel
UnmarkAllFormulas
UnmarkCutAncestors
prooftool
provers
congruence
CC
CC
MutCC
Eqn
InputEq
Pending
PropagEq
MutCC
Explainer
SimpleSmtSolver
eprover
EProver
EProver
escargot
impl
BackwardSuperpositionIndex
ClauseFeatureVec
ClauseFeatureVec
Cls
DiscrTree
DiscrTree
Constant
Label
Leaf
Node
Variable
EscargotLogger
EscargotState
ForwardSuperpositionIndex
Frequencies
Frequencies
FrequenciesBuilder
Index
IndexedClsSet
IndexedClsSet
InferenceRule
MaxPosLitIndex
PreprocessingRule
RedundancyRule
SelectedLitIndex
SimplificationRule
StandardInferences
AvatarSplitting
BackwardSubsumption
BackwardUnitRewriting
ClauseFactoring
Clausification
DuplicateDeletion
EqualityResolution
Factoring
ForwardSubsumption
ForwardUnitRewriting
OrderEquations
OrderedResolution
ReflModEqDeletion
ReflModEqIndex
ReflexivityDeletion
SubsumptionInterreduction
Superposition
TautologyDeletion
UnifyingEqualityResolution
VariableEqualityResolution
TermFeatureVec
TermFeatureVec
TermString
TermString
UnitRwrLhsIndex
fastSubsumption
getFOPositions
Escargot
Escargot
KBO
LPO
NonSplittingEscargot
QfUfEscargot
TermOrdering
iprover
IProver
IProverInput
IProverInstance
IProverOutput
Labels
TptpDerivationParser
leancop
LeanCoP
LeanCoP
maxsat
ExternalMaxSATSolver
MaxSATSolver
MaxSATSolver
MaxSat4j
MaxSat4j
MiFuMaX
MiniMaxSAT
OpenWBO
QMaxSAT
ToySAT
ToySolver
bestAvailableMaxSatSolver
metis
Metis
Metis
prover9
Prover9
Prover9
Prover9Importer
sat
DrupSolver
ExternalSATSolver
Glucose
Glucose
MiniSAT
PicoSAT
PicoSAT
SATSolver
Sat4j
RupListener
Sat4j
simp
AtomSimpLemma
EqSimpLemma
IffSimpLemma
NegAtomSimpLemma
QPropSimpProc
SimpEqResult
SimpEqResult
Prf
Refl
SimpIffResult
SimpIffResult
Prf
Refl
SimpLemmaProjection
SimpLemmas
SimpProc
SimpProver
SimpTactic
Simplifier
Simplifier
slakje
ExpToLKMethod
ExpToLKMethod
Heuristic
MG3iViaSAT
MG4ip
Slakje
Slakje
SlakjeLogger
heuristicDecidabilityInstantiation
smtlib
CVC4
CVC4
ExternalSmtlibProgram
UnexpectedTerminationException
SmtInterpol
SmtInterpol
SmtInterpolLogger
proxy
SmtInterpolSession
Z3
Z3
spass
SPASS
SPASS
InferenceParser
InferenceParser
vampire
Vampire
Vampire
VampireCASC
verit
FormulaInstance
VeriT
VeriT
alethe
toExpr
aletheQfUf
ReflexivityInstance
TransitivityInstance
transitivityAxioms
viper
aip
axioms
Axiom
AxiomFactory
DomainClosureAxioms
GeneralInductionAxioms
IndependentInductionAxioms
SequentialInductionAxioms
StandardInductionAxioms
StandardInductionAxioms
TipDomainClosureAxioms
UntrustedFunctionalInductionAxioms
UserDefinedInductionAxioms
AnalyticInductionProver
AnalyticInductionProver
ProverOptions
grammars
DefaultProvers
EnumeratingInstanceGenerator
IndElimProver
IndElimProver
InductionBUP
BupSequent
EndCut
IndCase
InductionBupSolver
InductionBupSolver
Canonical
Dls
Interpolation
InstanceTermGenerator
RandomInstanceGenerator
TreeGrammarInductionTactic
TreeGrammarProver
TreeGrammarProver
TreeGrammarProverOptions
TreeGrammarProverOptions
AddNormalizedFormula
NumProductionsWeight
Passthru
ProductionWeight
SmtEquationMode
SymbolicWeight
constructSIP
enumerateTerms
hSolveQBUP
indElimReversal
randomInstance
solveBupViaInterpolationBoundedDepth
solveBupViaInterpolationConcreteTerms
spin
AxiomGenerator
FormulaTester
Occurences
OccurrencesFinder
Positions
Positions
Spin
Spin
SpinOptions
asInductiveConst
constructorRules
isInductive
reflRules
AipOptions
Viper
ViperOptions
ViperOptions
IncrementalProver
OneShotProver
Prover
ResolutionProver
Session
Runners
BenchmarkRecorder
ExternalSMTLibSessionRunner
SMTLibSessionRunner
termRenaming
typeRenaming
SessionRunner
StackSessionRunner
SessionCommand
Ask
Assert
AssertLabelled
CheckSat
DeclareFun
DeclareSort
Pop
Push
SetLogic
SetOption
Tell
SessionCommand
extractIntroducedDefinitions
groundFreeVariables
mangleName
renameConstantsToFi
testing
CutReductionBenchmarkTools
AbstractLKtNorm
BogoElim
CERESEXP
ExpCutElim
LKCERES
LKMethod
LKReductive
LKtNorm
LKtNormA
LKtNormP
Method
LeanCoPTestCase
Prover9TestCase
RegressionTestCase
StepBlock
StepCondition
TestRun
Step
RegressionTests
TheoryTestCase
AllTheories
TheoryTestCase
TipTestCase
TptpTestCase
VeriTTestCase
clausifier
collectExperimentResults
computeStrategies
cutReductionBenchmark
dumpTermset
findNonTrivialTSTPExamples
TermSetStats
indElimBench
AbstractIndLKtNorm
AllTheories
BogoElim
IndLKReductive
IndLKtNorm
IndLKtNormA
IndLKtNormP
loadAndCompress
parseMethod
parseMode
primeCutElimBench
runOutOfProcess
sipReconstruct
testCutIntro
testExpansionImport
testInduction
StrategyNotApplicable
testLKToND
testLKToND2
testPi2CutIntro
testResolutionToExpansion
testTstpImport
testViper
utils
Counter
Doc
Doc
EitherHelpers
RichEither
ExceptionTag
ExternalProgram
LogHandler
LogHandler
Verbosity
default
silent
tstp
tstpWithMetrics
Logger
Logger
Maybe
Maybe
None
Some
Maybe0
Maybe1
MetricsPrinter
MetricsPrinterWithMessages
NameGenerator
NameGenerator
Statistic
Statistic
StreamUtils
TimeOutException
Tree
Tree
UNone
UOption
USome
generatedUpperSetInPO
help
linearizeStrictPartialOrder
quiet
runProcess
shortestPath
comparator
time
transitiveClosure
verbose
withTempFile
withTimeout
zipped
gapt
gapt
This is the API documentation for
GAPT
.
The main package is
gapt
.
Attributes
Members list
Clear all
Packages
package
gapt
In this article
Attributes
Members list
Packages