041-proving.rb revision b03747916bb00f7f1d3677cf02d244d25af4ba96
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehaserepository = Repository.find_by_path('default')
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase%w(v__T strict_partial_order).each do |ontology_name|
f198c0ec200763fe1b0db998cd9418f412be8361Tim Reddehase ontology = repository.ontologies.find_by_name(ontology_name)
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase Proof.new({ontology_id: ontology.id,
d60ddfb99765ab4fe956503f3f83d9c8f493eb99Tim Reddehase proof: {axiom_selection_method: 'manual_axiom_selection'}},
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase prove_asynchronously: false).save!
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehaseend
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehaseontology = repository.ontologies.find_by_name('v__T')
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehasetheorem = ontology.theorems.find_by_name('antisymmetric')
0dcf2700340141bc08344977e966e7ec095a8e8eTim ReddehaseProof.new({ontology_id: ontology.id,
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase theorem_id: theorem.id,
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase proof: {axiom_selection_method: 'manual_axiom_selection'}},
6876ece18854869a08606c12e0e814435fa73a29Tim Reddehase prove_asynchronously: false).save!
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehaseontology = repository.ontologies.find_by_name('SubclassToleranceOne')
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehasetheorem = ontology.theorems.find_by_name('beer < liquid')
0dcf2700340141bc08344977e966e7ec095a8e8eTim ReddehaseProof.new({ontology_id: ontology.id,
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase theorem_id: theorem.id,
6876ece18854869a08606c12e0e814435fa73a29Tim Reddehase proof: {axiom_selection_method: 'sine_axiom_selection',
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase sine_axiom_selection: {commonness_threshold: 1,
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase depth_limit: -1,
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase tolerance: 1}}},
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase prove_asynchronously: false).save!
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase
6876ece18854869a08606c12e0e814435fa73a29Tim Reddehaseontology = repository.ontologies.find_by_name('SubclassToleranceOnePointFive')
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehasetheorem = ontology.theorems.find_by_name('beer < liquid')
0dcf2700340141bc08344977e966e7ec095a8e8eTim ReddehaseProof.new({ontology_id: ontology.id,
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase theorem_id: theorem.id,
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase proof: {axiom_selection_method: 'sine_axiom_selection',
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase sine_axiom_selection: {commonness_threshold: 1,
6876ece18854869a08606c12e0e814435fa73a29Tim Reddehase depth_limit: -1,
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase tolerance: 1}}},
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase prove_asynchronously: false).save!
0dcf2700340141bc08344977e966e7ec095a8e8eTim Reddehase