http://www.w3.org/2000/10/swap/reason#variable
http://www.w3.org/2000/01/rdf-schema#range http://www.w3.org/2000/10/swap/reify#String
http://www.w3.org/2000/01/rdf-schema#label variable
http://www.w3.org/2000/01/rdf-schema#domain http://www.w3.org/2000/10/swap/reason#Binding
http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/1999/02/22-rdf-syntax-ns#Property
http://www.w3.org/2002/07/owl#FunctionalProperty
http://www.w3.org/2000/01/rdf-schema#comment 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.

http://www.w3.org/2000/10/swap/reason#component
http://www.w3.org/2000/01/rdf-schema#range http://www.w3.org/2000/10/swap/reason#Step
http://www.w3.org/2000/01/rdf-schema#label component
http://www.w3.org/2000/01/rdf-schema#domain http://www.w3.org/2000/10/swap/reason#Conjunction
http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/1999/02/22-rdf-syntax-ns#Property
http://www.w3.org/2000/01/rdf-schema#comment A step whose data was used in building this conjunction

http://www.w3.org/2000/10/swap/reason#rule
http://www.w3.org/2000/01/rdf-schema#range http://www.w3.org/2000/10/swap/reason#Step
http://www.w3.org/2000/01/rdf-schema#label rule
http://www.w3.org/2000/01/rdf-schema#domain http://www.w3.org/2000/10/swap/reason#Inference
http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/1999/02/22-rdf-syntax-ns#Property
http://www.w3.org/2002/07/owl#FunctionalProperty
http://www.w3.org/2000/01/rdf-schema#comment The inference step was performed using a rule (implication) given.

https://mtp.linked.solutions/
http://xmlns.com/foaf/0.1/topic https://mtp.linked.solutions/re

http://www.w3.org/2000/10/swap/reason#Proof
http://www.w3.org/2000/01/rdf-schema#label proof
http://www.w3.org/2000/01/rdf-schema#comment 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. .
http://www.w3.org/2000/01/rdf-schema#subClassOf http://www.w3.org/2000/10/swap/reason#Step

http://www.w3.org/2000/10/swap/reason#because
http://www.w3.org/2000/01/rdf-schema#range http://www.w3.org/2000/10/swap/reason#Step
http://www.w3.org/2000/01/rdf-schema#label from
http://www.w3.org/2000/01/rdf-schema#domain http://www.w3.org/2000/10/swap/reason#Extraction
http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/1999/02/22-rdf-syntax-ns#Property
http://www.w3.org/2000/01/rdf-schema#comment gives the step whose data was input to this step.

http://www.w3.org/2000/10/swap/reason#gives
http://www.w3.org/2000/01/rdf-schema#range http://www.w3.org/2000/10/swap/reify#Formula
http://www.w3.org/2000/01/rdf-schema#label gives
http://www.w3.org/2000/01/rdf-schema#domain http://www.w3.org/2000/10/swap/reason#Step
http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/1999/02/22-rdf-syntax-ns#Property
http://www.w3.org/2000/01/rdf-schema#comment 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

http://www.w3.org/2000/10/swap/reason#source
http://www.w3.org/2000/01/rdf-schema#range http://www.w3.org/2000/10/swap/pim/soc#Work
http://www.w3.org/2000/01/rdf-schema#label source
http://www.w3.org/2000/01/rdf-schema#domain http://www.w3.org/2000/10/swap/reason#Parsing
http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/1999/02/22-rdf-syntax-ns#Property
http://www.w3.org/2002/07/owl#FunctionalProperty
http://www.w3.org/2000/01/rdf-schema#comment The source document which was parsed.

http://www.w3.org/2000/10/swap/reason#boundTo
http://www.w3.org/2000/01/rdf-schema#range http://www.w3.org/2000/10/swap/reify#Term
http://www.w3.org/2000/01/rdf-schema#label bound to
http://www.w3.org/2000/01/rdf-schema#domain http://www.w3.org/2000/10/swap/reason#Binding
http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/1999/02/22-rdf-syntax-ns#Property
http://www.w3.org/2002/07/owl#FunctionalProperty
http://www.w3.org/2000/01/rdf-schema#comment This binding binds its variable to this term.

http://www.w3.org/2000/10/swap/reason#args
http://www.w3.org/2000/01/rdf-schema#label A human-readable representation of the arguments given on the command line
http://www.w3.org/2000/01/rdf-schema#domain http://www.w3.org/2000/10/swap/reason#Commandline
http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/1999/02/22-rdf-syntax-ns#Property
http://www.w3.org/2002/07/owl#FunctionalProperty

http://www.w3.org/2000/10/swap/reason#evidence
http://www.w3.org/2000/01/rdf-schema#range http://www.w3.org/1999/02/22-rdf-syntax-ns#List
http://www.w3.org/2000/01/rdf-schema#label antecedents
http://www.w3.org/2000/01/rdf-schema#domain http://www.w3.org/2000/10/swap/reason#Inference
http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/1999/02/22-rdf-syntax-ns#Property
http://www.w3.org/2002/07/owl#FunctionalProperty
http://www.w3.org/2000/01/rdf-schema#comment 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.

http://www.w3.org/2000/10/swap/reason#CommandLine
http://www.w3.org/2000/01/rdf-schema#subClassOf http://www.w3.org/2000/10/swap/reason#Step

http://www.w3.org/2000/10/swap/reason#Step
http://www.w3.org/2000/01/rdf-schema#label proof step
http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/2000/01/rdf-schema#Class
http://www.w3.org/2000/01/rdf-schema#comment A step in a proof. See :gives for the arc to the formula actually proved at this step.

http://www.w3.org/2000/10/swap/reason#Inference
http://www.w3.org/2000/01/rdf-schema#label GMP Inference
http://www.w3.org/2000/01/rdf-schema#subClassOf http://www.w3.org/2000/10/swap/reason#Step

https://mtp.linked.solutions/re
http://purl.org/dc/terms/source https://github.com/linked-solutions/prefix.cc-harvest/master
http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/2002/07/owl#Ontology
http://purl.org/vocab/vann/preferredNamespaceUri http://www.w3.org/2000/10/swap/reason#
http://purl.org/vocab/vann/preferredNamespacePrefix re
http://rdfs.org/ns/void#triples 69

http://www.w3.org/2000/10/swap/reason#Binding
http://www.w3.org/2000/01/rdf-schema#label binding
http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/2000/01/rdf-schema#Class
http://www.w3.org/2000/01/rdf-schema#comment 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.

http://www.w3.org/2000/10/swap/reason#Parsing
http://www.w3.org/2000/01/rdf-schema#label parsing
http://www.w3.org/2000/01/rdf-schema#comment The formula given was derived from parsing a resource.
http://www.w3.org/2000/01/rdf-schema#subClassOf http://www.w3.org/2000/10/swap/reason#Step

http://www.w3.org/2000/10/swap/reason#Extraction
http://www.w3.org/2000/01/rdf-schema#label Conjunction elimination
http://www.w3.org/2000/01/rdf-schema#comment 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).
http://www.w3.org/2000/01/rdf-schema#subClassOf http://www.w3.org/2000/10/swap/reason#Step

http://www.w3.org/2000/10/swap/reason#Conjunction
http://www.w3.org/2000/01/rdf-schema#label The step of conjunction introduction: taking a bunch of compent statements and building a formula from them.
http://www.w3.org/2000/01/rdf-schema#subClassOf http://www.w3.org/2000/10/swap/reason#Step