Class Tree

Property Tree

Class Descriptions

Class: http://www.w3.org/2002/07/owl#Thing
Thing
Possibly subject of: variable, component, args, because, evidence, gives, boundTo, rule, source
Object of: args
Possibly object of: variable, evidence, gives, boundTo, source, component, because, rule
Class: http://www.w3.org/2000/10/swap/reason#Binding
binding
A binding is given eg in a proof or query result. The binding specifies which variable was bound (:variable), and what term it was bound to.
Thing
Subject of: variable, boundTo
Possibly subject of: component, args, because, evidence, gives, rule, source
Object of: args
Possibly object of: variable, component, because, evidence, gives, boundTo, rule, source
Class: http://www.w3.org/2000/10/swap/reason#Commandline
Thing
Subject of: args
Possibly subject of: variable, component, because, evidence, gives, boundTo, rule, source
Object of: args
Possibly object of: variable, component, because, evidence, gives, boundTo, rule, source
Class: http://www.w3.org/2000/10/swap/reason#Step
proof step
A step in a proof. See :gives for the arc to the formula actually proved at this step.
Thing
Subject of: gives
Possibly subject of: variable, args, boundTo, component, because, evidence, rule, source
Object of: component, args, because, rule
Possibly object of: variable, evidence, gives, boundTo, source
Class: http://www.w3.org/2000/10/swap/reason#Conjunction
The step of conjunction introduction: taking a bunch of compent statements and building a formula from them.
proof·step
Subject of: component, gives
Possibly subject of: variable, args, because, evidence, boundTo, rule, source
Object of: component, args, because, rule
Possibly object of: variable, evidence, gives, boundTo, source
Class: http://www.w3.org/2000/10/swap/reason#CommandLine
proof·step
Subject of: gives
Possibly subject of: variable, component, args, because, evidence, boundTo, rule, source
Object of: component, args, because, rule
Possibly object of: variable, evidence, gives, boundTo, source
Class: http://www.w3.org/2000/10/swap/reason#Proof
proof
A Proof step is the last step in the proof, a step which :gives that which was to be proved. Typically a document will assert just one :Proof, which a checker can then check and turn into the Formula proved - Q.E.D. .
proof·step
Subject of: gives
Possibly subject of: variable, component, args, because, evidence, boundTo, rule, source
Object of: component, args, because, rule
Possibly object of: variable, evidence, gives, boundTo, source
Class: http://www.w3.org/2000/10/swap/reason#Parsing
parsing
The formula given was derived from parsing a resource.
proof·step
Subject of: gives, source
Possibly subject of: variable, component, args, because, evidence, boundTo, rule
Object of: component, args, because, rule
Possibly object of: variable, evidence, gives, boundTo, source
Class: http://www.w3.org/2000/10/swap/reason#Extraction
Conjunction elimination
The step of taking one statement out of a formula. The step is identified by the :gives formula (the statement) and the :because step's :gives formula (the formula extracted from).
proof·step
Subject of: because, gives
Possibly subject of: variable, component, args, evidence, boundTo, rule, source
Object of: component, args, because, rule
Possibly object of: variable, evidence, gives, boundTo, source
Class: http://www.w3.org/2000/10/swap/reason#Inference
GMP Inference
proof·step
Subject of: evidence, gives, rule
Possibly subject of: variable, component, args, because, boundTo, source
Object of: component, args, because, rule
Possibly object of: variable, evidence, gives, boundTo, source

Property Descriptions

Annotation-Property: http://www.w3.org/2000/01/rdf-schema#label
Annotation-Property: http://purl.org/dc/elements/1.1/title
Annotation-Property: http://www.w3.org/2000/01/rdf-schema#seeAlso
Annotation-Property: http://www.w3.org/2002/07/owl#versionInfo
Annotation-Property: http://purl.org/dc/elements/1.1/description
Annotation-Property: http://www.w3.org/2000/01/rdf-schema#comment
Annotation-Property: http://www.w3.org/2000/01/rdf-schema#isDefinedBy
Object-Property: http://www.w3.org/2000/10/swap/reason#variable
variable
The given string is that used as the identifier of the variable which is bound by this binding. The variable name has to be given as a string, rather than the variable being put here, or the variable would be treated as a variable.
Functional
Domain: binding
Range: String
Object-Property: http://www.w3.org/2000/10/swap/reason#component
component
A step whose data was used in building this conjunction
Domain: The·step·of·conjunction·introduction:·
····taking·a·bunch·of·compent·statements
····and·building·a·formula·from·them.
Range: proof·step
Object-Property: http://www.w3.org/2000/10/swap/reason#args
A human-readable representation of the arguments given on the command line
Functional
Domain: Commandline
Range: Thing
Object-Property: http://www.w3.org/2000/10/swap/reason#because
from
gives the step whose data was input to this step.
Domain: Conjunction·elimination
Range: proof·step
Object-Property: http://www.w3.org/2000/10/swap/reason#evidence
antecedents
The :evidence for a GMP inference step is a list of formulas, each proved by other means, which combined entail the result of making the given substitution in the antecedent of the rule.
Functional
Domain: GMP·Inference
Range: List
Object-Property: http://www.w3.org/2000/10/swap/reason#gives
gives
The proof step gives the formula as a result. For some steps, like extraction of a statement from a formula, it is essential to give the result formula in a proof to define what step has been taken. For other steps, such as GMP inference, the specification of the rule and bindings defines the result, and so the proof can still be checked if the reason:gives ars
Domain: proof·step
Range: Formula
Object-Property: http://www.w3.org/2000/10/swap/reason#boundTo
bound to
This binding binds its variable to this term.
Functional
Domain: binding
Range: Term
Object-Property: http://www.w3.org/2000/10/swap/reason#rule
rule
The inference step was performed using a rule (implication) given.
Functional
Domain: GMP·Inference
Range: proof·step
Object-Property: http://www.w3.org/2000/10/swap/reason#source
source
The source document which was parsed.
Functional
Domain: parsing
Range: Work