theorem.yml revision 9940047ec4fd0ef151dfddd4253534eafa8c900c
---
http_interactions:
- request:
method: get
body:
encoding: US-ASCII
string: ''
headers:
Accept-Encoding:
- gzip;q=1.0,deflate;q=0.6,identity;q=0.3
Accept:
- "*/*"
User-Agent:
- Ruby
response:
status:
code: 200
message: OK
headers:
Server:
- nginx/1.6.2
Date:
- Sat, 04 Apr 2015 19:35:18 GMT
Content-Type:
Content-Length:
- '1379'
Last-Modified:
- Thu, 02 Apr 2015 10:03:34 GMT
Connection:
- keep-alive
Etag:
- '"551d13f6-563"'
Strict-Transport-Security:
- max-age=31536000
X-Frame-Options:
- DENY
Accept-Ranges:
- bytes
body:
encoding: ASCII-8BIT
string: !binary |-
ewogICJpZCI6ICJodHRwczovL21hc3RlcnRoZXNpcy5yaWdodHNyZXN0cmlj
dGVkLmNvbS9vbnRvaHViL3RoZW9yZW0uanNvbiMiLAogICIkc2NoZW1hIjog
Imh0dHA6Ly9qc29uLXNjaGVtYS5vcmcvZHJhZnQtMDQvc2NoZW1hIyIsCiAg
InRpdGxlIjogIlRoZW9yZW0iLAogICJkZXNjcmlwdGlvbiI6ICJBIHRoZW9y
ZW0gaW5zaWRlIG9mIGFuIG9udG9sb2d5IiwKICAidHlwZSI6ICJvYmplY3Qi
LAogICJwcm9wZXJ0aWVzIjogewogICAgImlyaSI6IHsKICAgICAgImRlc2Ny
aXB0aW9uIjogIlRoZSB1bmlxdWUgaWRlbnRpZmllciBmb3IgdGhlIHRoZW9y
ZW0iLAogICAgICAidHlwZSI6ICJzdHJpbmciLAogICAgICAiZm9ybWF0Ijog
InVyaSIKICAgIH0sCiAgICAibmFtZSI6IHsKICAgICAgImRlc2NyaXB0aW9u
IjogIlRoZSBuYW1lIG9mIHRoZSB0aGVvcmVtIOKAlCB1c3VhbGx5IGF1dG8t
Z2VuZXJhdGVkLiIsCiAgICAgICJ0eXBlIjogInN0cmluZyIKICAgIH0sCiAg
ICAiZGVmaW5pdGlvbiI6IHsKICAgICAgImRlc2NyaXB0aW9uIjogIlRoZSBk
ZWZpbml0aW9uIG9mIHRoZSB0aGVvcmVtIiwKICAgICAgInR5cGUiOiAic3Ry
aW5nIgogICAgfSwKICAgICJldmFsdWF0aW9uX3N0YXRlIjogewogICAgICAi
ZGVzY3JpcHRpb24iOiAiVGhlIGN1cnJlbnQgc3RhdGUgb2YgdGhlIHByb29m
IGV2YWx1YXRpb24iLAogICAgICAidHlwZSI6ICJzdHJpbmciLAogICAgICAi
ZW51bSI6IFsgImRvbmUiLCAiZmFpbGVkIiwgInBlbmRpbmciLCAicHJvY2Vz
c2luZyIgXQogICAgfSwKICAgICJwcm9vZl9zdGF0dXMiOiB7ICIkcmVmIjog
InJlZmVyZW5jZXMuanNvbiMvZGVmaW5pdGlvbnMvcHJvb2Zfc3RhdHVzIiB9
LAogICAgIm9udG9sb2d5IjogeyAiJHJlZiI6ICJyZWZlcmVuY2VzLmpzb24j
L2RlZmluaXRpb25zL29udG9sb2d5IiB9LAogICAgInN5bWJvbHMiOiB7CiAg
ICAgICJkZXNjcmlwdGlvbiI6ICJSZWZlcmVuY2UgdG8gYWxsIHN5bWJvbHMg
dXNlZCBpbiB0aGlzIHRoZW9yZW0iLAogICAgICAidHlwZSI6ICJzdHJpbmci
LAogICAgICAiZm9ybWF0IjogInVyaSIKICAgIH0sCiAgICAicHJvb2ZfYXR0
ZW1wdHMiOiB7CiAgICAgICJkZXNjcmlwdGlvbiI6ICJSZWZlcmVuY2UgdG8g
YWxsIHByb29mIGF0dGVtcHRzIGZvciB0aGlzIHRoZW9yZW0iLAogICAgICAi
dHlwZSI6ICJzdHJpbmciLAogICAgICAiZm9ybWF0IjogInVyaSIKICAgIH0K
ICB9LAogICJyZXF1aXJlZCI6IFsKICAgICJpcmkiLAogICAgIm5hbWUiLAog
ICAgImRlZmluaXRpb24iLAogICAgImV2YWx1YXRpb25fc3RhdGUiLAogICAg
InByb29mX3N0YXR1cyIsCiAgICAib250b2xvZ3kiLAogICAgInN5bWJvbHMi
LAogICAgInByb29mX2F0dGVtcHRzIgogIF0KfQo=
http_version:
recorded_at: Sat, 04 Apr 2015 19:35:18 GMT
- request:
method: get
body:
encoding: US-ASCII
string: ''
headers:
Accept-Encoding:
- gzip;q=1.0,deflate;q=0.6,identity;q=0.3
Accept:
- "*/*"
User-Agent:
- Ruby
response:
status:
code: 200
message: OK
headers:
Server:
- nginx/1.6.2
Date:
- Sat, 04 Apr 2015 19:35:18 GMT
Content-Type:
Content-Length:
- '6367'
Last-Modified:
- Thu, 02 Apr 2015 10:02:57 GMT
Connection:
- keep-alive
Etag:
- '"551d13d1-18df"'
Strict-Transport-Security:
- max-age=31536000
X-Frame-Options:
- DENY
Accept-Ranges:
- bytes
body:
encoding: UTF-8
string: |
{
"$schema": "http://json-schema.org/draft-04/schema#",
"definitions": {
"repository": {
"description": "Reference to a repository",
"type": "object",
"properties": {
"name": {
"description": "The name of the repository",
"type": "string"
},
"iri": {
"description": "The unique identifier of the repository",
"type": "string",
"format": "uri"
}
}
},
"logic": {
"description": "Reference to a logic",
"type": "object",
"properties": {
"name": {
"description": "The name of the logic",
"type": "string"
},
"iri": {
"description": "The unique identifier of the logic",
"type": "string",
"format": "uri"
}
}
},
"ontology": {
"description": "Reference to an ontology",
"type": "object",
"properties": {
"name": {
"description": "The name of the ontology",
"type": "string"
},
"iri": {
"description": "The unique identifier of the ontology",
"type": "string",
"format": "uri"
}
}
},
"license_model": {
"description": "Reference to a license model",
"type": "object",
"properties": {
"name": {
"description": "The name of the license model",
"type": "string"
},
"iri": {
"description": "The unique identifier of the license model",
"type": "string",
"format": "uri"
}
}
},
"formality_level": {
"description": "Reference to a formality level",
"type": "object",
"properties": {
"name": {
"description": "The name of the formality level",
"type": "string"
},
"iri": {
"description": "The unique identifier of the formality level",
"type": "string",
"format": "uri"
}
}
},
"ontology_type": {
"description": "Reference to an ontology type",
"type": "object",
"properties": {
"name": {
"description": "The name of the ontology type",
"type": "string"
},
"iri": {
"description": "The unique identifier of the ontology type",
"type": "string",
"format": "uri"
}
}
},
"ontology_version": {
"description": "Reference to an ontology-version",
"type": "object",
"properties": {
"number": {
"description": "The version number of the version of the ontology",
"type": "integer"
},
"iri": {
"description": "The unique identifier of the ontology-version",
"type": "string",
"format": "uri"
}
}
},
"logic_mapping": {
"description": "Reference to a mapping between logics",
"type": "object",
"properties": {
"iri": {
"description": "The unique identifier of the logic mapping",
"type": "string",
"format": "uri"
}
}
},
"mapping": {
"description": "Reference to a mapping",
"type": "object",
"properties": {
"name": {
"description": "The name of the mapping",
"type": "string"
},
"iri": {
"description": "The unique identifier of the mapping",
"type": "string",
"format": "uri"
}
}
},
"sentence": {
"description": "Reference to a sentence",
"type": "object",
"properties": {
"name": {
"description": "The name of the sentence",
"type": "string"
},
"iri": {
"description": "The unique identifier of the sentence",
"type": "string",
"format": "uri"
}
}
},
"symbol": {
"description": "Reference to a symbol",
"type": "object",
"properties": {
"name": {
"description": "The name of the symbol",
"type": "string"
},
"iri": {
"description": "The unique identifier of the symbol",
"type": "string",
"format": "uri"
}
}
},
"theorem": {
"description": "Reference to a theorem",
"type": "object",
"properties": {
"name": {
"description": "The name of the theorem",
"type": "string"
},
"iri": {
"description": "The unique identifier of the theorem",
"type": "string",
"format": "uri"
}
}
},
"proof_attempt": {
"description": "Reference to a proof attempt",
"type": "object",
"properties": {
"iri": {
"description": "The unique identifier of the proof attempt",
"type": "string",
"format": "uri"
},
"number": {
"description": "The number of the proof attempt relative to its theorem",
"type": "integer"
}
}
},
"proof_status": {
"description": "Reference to a proof status",
"type": "object",
"properties": {
"iri": {
"description": "The unique identifier of the proof status",
"type": "string",
"format": "uri"
},
"identifier": {
"description": "The identifier of the proof status",
"type": "string"
},
"name": {
"description": "The name of the proof status (human-readable)",
"type": "string"
}
}
},
"prover_output": {
"description": "Reference to a prover output",
"type": "object",
"properties": {
"iri": {
"description": "The unique identifier of the prover output",
"type": "string",
"format": "uri"
}
}
},
"proof_attempt_configuration": {
"description": "Reference to a proof attempt configuration",
"type": "object",
"properties": {
"iri": {
"description": "The unique identifier of the proof attempt configuration",
"type": "string",
"format": "uri"
}
}
}
}
}
http_version:
recorded_at: Sat, 04 Apr 2015 19:35:18 GMT
recorded_with: VCR 2.9.3