Action-2009-001

From Inference Web

Jump to: navigation, search

{{#vardefine:category|Thing}}{{#vardefine:templatename|o.thing}}{{#vardefine:package|smwbp_ontology_templates}}

warning.pngEmpty strings are not accepted. ({{#vardefine:ns| }}{{#vardefine:p|type }}{{#vardefine:v|Action }}) [ Edit ] {{#vardefine:ns| }}{{#vardefine:p|homepage }}{{#vardefine:v| }} {{#vardefine:ns| }}{{#vardefine:p|description }}{{#vardefine:v|how to deal with a pml file containing a Forrest of proofs while we typically expect one proof. }} {{#vardefine:ns| }}{{#vardefine:p|location }}{{#vardefine:v| }} {{#vardefine:ns| }}{{#vardefine:p|relation }}{{#vardefine:v|TPTP-IW }} {{#vardefine:ns| }}{{#vardefine:p|tag }}{{#vardefine:v| }} {{#vardefine:ns| }}{{#vardefine:p|alias }}{{#vardefine:v| }} {{#vardefine:ns| }}{{#vardefine:p|equal_to }}{{#vardefine:v| }}
[[Category:]]

log

03:46, 22 April 2009 (UTC) - from Cynthia's email

I did not check the value of "Output", but I do from now on.
This should solve the problem for these EP proofs.

But some EQP proofs in LAT domain have the same "multiple roots"
problem but they all have output of "Refutation 0.1s". They are
EQP proof for problems LAT006-1, 8-1, 12-1, 13-1, 14-1, 21-1, 22-1,
23-1, 26-1, 27-1, 32-1, 33-1, 34-1, 38-1, 40-1, 43-1, 45-1, 89-1,
90-1, 91-1, 148-1, 162-1, 168-1.

A few Vampire 10.0 and VampireLT 10.0 proofs in NUM still have the
error of "expecting COMMA, found ')'". They are:
NUM375+1.010&System=Vampire---10.0
NUM375+1.010&System=VampireLT---10.0
NUM375+1.015&System=Vampire---10.0
NUM375+1.015&System=VampireLT---10.0
NUM375+1.020&System=Vampire---10.0
NUM375+1.020&System=VampireLT---10.0
NUM375+1.025&System=VampireLT---10.0
NUM376+1.010&System=Vampire---10.0.
NUM376+1.010&System=VampireLT---10.0
NUM376+1.015&System=Vampire---10.0
NUM376+1.020&System=Vampire---10.0
UM376+1.030&System=VampireLT---10.0

A few SInE proofs in NUM still have "unknown status value: 'sab'" error:
NUM375+1.010&System=SInE---0.3
NUM375+1.015&System=SInE---0.3
NUM375+1.025&System=SInE---0.3.
NUM375+1.030&System=SInE---0.3
NUM376+1.010&System=SInE---0.3
NUM376+1.015&System=SInE---0.3
NUM376+1.025&System=SInE---0.3
NUM376+1.030&System=SInE---0.3
NUM377+1.010&System=SInE---0.3

CSR, SWC and SWV domain were retranslated without any problem.
More to come.
Facts about Action-2009-001RDF feed
Namewarning.pngEmpty strings are not accepted.
Personal tools
Navigation