Lurch Deductive Engine
Tutorials
Connections among LCs
Constructing LCs
Free and bound variables
LC tree hierarchies
Lurch Node REPL
Methods in each LC subclass
Pattern matching
Serialization and attributes of LCs
Classes
C
Application
F
operands
F
operator
C
Array
F
last
F
without
F
range
F
seq
C
BindingEnvironment
C
BindingExpression
C
CNFProp
M
signature
M
switchVarSymbol
F
hasCNFform
F
simplify
F
toAlgebraic
F
toArray
F
toEnglish
F
fromLC
F
toCNF
F
toVar
C
Connection
M
IDs
F
attr
F
clearAttributes
F
getAttribute
F
getAttributeKeys
F
handleIDChange
F
hasAttribute
F
remove
F
setAttribute
F
source
F
target
F
create
F
transferConnections
F
withID
C
Constraint
M
expression
M
pattern
F
afterSubstituting
F
children
F
complexity
F
complexityName
F
copy
F
deBruijnDecode
F
deBruijnEncode
F
equals
F
isAnInstantiation
F
toString
C
Declaration
F
body
F
copy
F
removeBody
F
setBody
F
symbols
C
Environment
F
conclusions
F
inferences
C
EventTarget
F
emit
C
Expression
F
getOutermost
F
isAConclusionIn
F
isOutermost
F
value
C
LogicConcept
F
conditionalForm
F
enableFeedback
F
feedback
F
hasOnlyClaimAncestors
F
isSymbol
F
markDirty
F
matches
F
origin
F
toPutdown
F
fromPutdown
C
Map
F
deepCopy
C
MathConcept
M
IDs
M
className
M
subclasses
F
ID
F
accessibles
F
accessiblesIterator
F
address
F
allButFirstChild
F
allButLastChild
F
ancestors
F
ancestorsIterator
F
ancestorsSatisfying
F
asA
F
attr
F
binds
F
changeID
F
child
F
children
F
childrenSatisfying
F
clearAttributes
F
clearIDs
F
connectTo
F
copy
F
copyAttributesFrom
F
descendantsIterator
F
descendantsSatisfying
F
equals
F
feedback
F
firstChild
F
freeSymbolNames
F
getAttribute
F
getAttributeKeys
F
getConnectionIDs
F
getConnectionIDsIn
F
getConnectionIDsOut
F
getConnections
F
getConnectionsIn
F
getConnectionsOut
F
hasAncestorSatisfying
F
hasAttribute
F
hasChildSatisfying
F
hasDescendantSatisfying
F
idIsTracked
F
index
F
indexInParent
F
insertChild
F
interpret
F
interpretation
F
isA
F
isAccessibleTo
F
isAtomic
F
isDirty
F
isEarlierThan
F
isFree
F
isFreeToReplace
F
isInTheScopeOf
F
isLaterThan
F
lastChild
F
makeIntoA
F
markDirty
F
nextInTree
F
nextSibling
F
numChildren
F
occursFree
F
parent
F
popChild
F
preOrderIterator
F
preOrderTraversal
F
previousInTree
F
previousSibling
F
pushChild
F
remove
F
removeChild
F
removeConnections
F
replaceFree
F
replaceWith
F
scope
F
scopeIterator
F
setAttribute
F
setChildren
F
setID
F
shiftChild
F
toJSON
F
toSmackdown
F
toString
F
trackConnections
F
trackIDs
F
transferConnectionsTo
F
unmakeIntoA
F
unshiftChild
F
untrackIDs
F
addSubclass
F
feedback
F
fromJSON
F
fromSmackdown
F
instanceWithID
F
typeAttributeKey
E
wasChanged
E
wasInserted
E
wasRemoved
E
willBeChanged
E
willBeInserted
E
willBeRemoved
C
NewSymbolStream
F
avoid
F
copy
F
next
F
nextN
C
Problem
M
length
F
add
F
afterSubstituting
F
copy
F
empty
F
equals
F
firstSolution
F
isSolvable
F
numSolutions
F
plus
F
remove
F
solutions
F
substitute
F
toString
F
without
C
PropositionalForm
F
CNF
F
isAClassicalTautology
F
isAnIntuitionisticTautology
F
isAtomic
F
isConditional
F
isConstantTrue
F
negatedCNF
F
atomic
F
conditional
F
constantTrue
F
fromConclusion
F
fromConclusionsIn
F
sequent
C
Sequent
M
attributesToKeep
F
conclusion
F
copy
F
originalConclusion
F
originalPremises
F
premises
C
Set
F
difference
F
equals
F
intersection
F
isSubset
F
isSuperset
F
subset
F
symmetricDifference
F
union
C
Solution
F
add
F
afterSubstituting
F
complete
F
copy
F
domain
F
equals
F
get
F
plus
F
restrict
F
restricted
F
substitute
F
toString
C
SourceMap
F
dataForMarker
F
modified
F
modifiedLineAndColumn
F
modifiedPosition
F
modify
F
nextMarker
F
nextModificationPosition
F
source
F
sourceLineAndColumn
F
sourcePosition
F
debugCode
F
isMarker
C
Substitution
M
expression
M
metavariable
F
afterSubstituting
F
appliedTo
F
applyTo
F
copy
F
deBruijnDecode
F
deBruijnEncode
F
equals
F
metavariableNames
F
substitute
F
toString
C
Symbol
F
insertChild
F
text
F
toString
F
value
C
TreeIndexer
F
define
F
delete
F
get
F
show
F
update
F
updateAll
Modules
M
ExpressionFunctions
M
alphaEquivalent
M
alphaRenamed
M
applicationEF
M
applyEF
M
arityOfEF
M
betaReduce
M
bodyOfEF
M
canBetaReduce
M
constantEF
M
expressionFunction
M
expressionFunctionApplication
M
fullBetaReduce
M
isAnEF
M
isAnEFA
M
newEF
M
newEFA
M
parametersOfEF
M
projectionEF
M
GlobalValidation
M
isDopplegangerOf
F
cacheFormulaDomainInfo
F
copyEquation
F
diff
F
eq2chain
F
forbiddenWeeny
F
getCaselikeRules
F
getUserPropositions
F
insertInstantiation
F
insertSymmetricEquivalences
F
instantiate
F
instantiateTransitives
F
isBadInstantiation
F
markFlaggedDeclarations
F
matchGivens
F
matchPropositions
F
patternForm
F
processBIHs
F
processCases
F
processChains
F
processDomains
F
processEquations
F
reverseEquation
F
splitChains
F
splitEquations
F
tidyProperNames
F
upgradeChains
F
validate
M
Interpretation
M
systemConstants
F
addSystemDeclarations
F
assignProperNames
F
canonicalizeBindings
F
interpret
F
markDeclaredSymbols
F
moveDeclaresToTop
F
processBindings
F
processDeclarationBodies
F
processLetEnvironments
F
processRules
F
processTheorems
F
removeTrailingGivens
F
renameBindings
F
replaceBindings
F
splitConclusions
M
Lode
F
list
M
Matching
F
allInstantiations
F
allOptionalInstantiations
M
Metavariables
M
metavariable
F
containsAMetavariable
F
metavariableNamesIn
F
metavariablesIn
M
Parsing
M
arithmeticToCAS
M
isNegationOfArithmetic
F
processShorthands
F
makeParser
F
numericToCAS
F
parseLines
F
partition
M
Reporting
M
Scoping
F
addImplicitDeclaration
F
addScopeError
F
clearImplicitDeclarations
F
clearScopeErrors
F
declareGlobal
F
declareInAncestor
F
declareWhenSeen
F
doNotDeclare
F
implicitDeclarations
F
removeImplicitDeclaration
F
scopeErrors
F
validate
M
Utilities
F
checkExtension
F
checkFolder
F
commonInitialSlice
F
hex2rgb
F
indent
F
lineNum
F
rgb2hex
F
subscript
F
tab
F
timer
M
Validation
F
clearOptions
F
clearResult
F
functionToTool
F
getOptions
F
installTool
F
installedTool
F
installedToolNames
F
result
F
setOptions
F
setResult
F
validate
M
deBruijn
M
deBruijn
M
free
M
isEncodedBinding
M
numberOfOccurrences
F
adjustIndices
F
decodeExpression
F
decodeSymbol
F
encodeExpression
F
encodeSymbol
F
encodedIndices
F
equal
M
z3
Namespaces
N
BindingInterface
M
addTo
M
allAreSymbols
M
binds
M
body
M
boundSymbolNames
M
boundSymbols
N
CNF
F
and
F
constantFalse
F
constantTrue
F
isSatisfiable
F
or
F
proposition
N
Database
M
filterByMetadata
M
getCode
M
getCodeWithoutIncludes
M
getMetadata
M
getObject
M
getObjects
M
keys
M
keysPaths
M
keysStartingWith
N
Extensions
F
Declaration#allProps
F
Declaration#letsInScope
F
Declaration#lookup
F
Declaration#prop
F
Environment#catalog
F
Environment#cnf
F
Environment#letInferences
F
Environment#scopes
F
Expression#allProps
F
Expression#lookup
F
Expression#prop
F
LogicConcept#Insts
F
LogicConcept#Parts
F
LogicConcept#attributes
F
LogicConcept#bindings
F
LogicConcept#chains
F
LogicConcept#declarations
F
LogicConcept#descendantsSatisfyingIterator
F
LogicConcept#environments
F
LogicConcept#equations
F
LogicConcept#find
F
LogicConcept#forSomes
F
LogicConcept#formulas
F
LogicConcept#getDeclares
F
LogicConcept#getRules
F
LogicConcept#getTheorems
F
LogicConcept#insertAfter
F
LogicConcept#insertBefore
F
LogicConcept#isAChain
F
LogicConcept#isAComment
F
LogicConcept#isADeclaration
F
LogicConcept#isAForSome
F
LogicConcept#isALet
F
LogicConcept#isALetEnvironment
F
LogicConcept#isAProposition
F
LogicConcept#isAStatement
F
LogicConcept#isAnEquation
F
LogicConcept#letAncestors
F
LogicConcept#lets
F
LogicConcept#mentions
F
LogicConcept#metavars
F
LogicConcept#negate
F
LogicConcept#propositions
F
LogicConcept#results
F
LogicConcept#root
F
LogicConcept#setResult
F
LogicConcept#slice
F
LogicConcept#some
F
LogicConcept#statements
F
LogicConcept#symbols
F
LogicConcept#toAlgebraic
F
LogicConcept#toEnglish
F
LogicConcept#toNice
F
LogicConcept#toggleGiven
F
LurchSymbol#properName
F
LurchSymbol#rename
N
Formula
M
cachedInstantiation
F
addCachedInstantiation
F
allCachedInstantiations
F
allPossibleInstantiations
F
clearCachedInstantiations
F
domain
F
from
F
hasDeclarationCapture
F
instantiate
F
possibleSufficientInstantiations
N
JSON
F
copy
F
equals
N
ValidationTools
F
CASValidator
F
arithmeticValidator
F
classicalPropositionalValidator
F
intuitionisticPropositionalValidator
Globals
M
LurchOptions
M
addIndex
M
addLurchIndices
F
deepCopyJson
M
predictableStringify
F
putdownSymbolText
Module
z3
Lurch integration with z3