From e80b93ca958bdbeb28959029868f6193b39a3f19 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 24 Jun 2013 19:58:37 -0400 Subject: Support for TPTP's TFF0 (with arithmetic) This commit reverses an "SZS ontology compliance hack" that was done for CASC-24 this year, and adds a TPTP pretty-printer which is capable of outputting results in the TPTP way (rather than the SMT way). This commit includes minor changes to the Expr package to add obvious missing functionality, and to fix the way expressions with builtin operators are made. These changes are truly a _fix_, the implementation had not been properly aligned with the design vision for some corner cases. --- test/regress/regress0/tptp/KRS018+1.p | 55 +++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 test/regress/regress0/tptp/KRS018+1.p (limited to 'test/regress/regress0/tptp/KRS018+1.p') diff --git a/test/regress/regress0/tptp/KRS018+1.p b/test/regress/regress0/tptp/KRS018+1.p new file mode 100644 index 000000000..91039877b --- /dev/null +++ b/test/regress/regress0/tptp/KRS018+1.p @@ -0,0 +1,55 @@ +%------------------------------------------------------------------------------ +% File : KRS018+1 : TPTP v5.5.0. Released v3.1.0. +% Domain : Knowledge Representation (Semantic Web) +% Problem : Nothing can be defined using OWL Lite restrictions +% Version : Especial. +% English : + +% Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe +% : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW +% Source : [Bec03] +% Names : consistent_I5.2-Manifest001 [Bec03] + +% Status : Satisfiable +% Rating : 0.00 v4.1.0, 0.25 v4.0.1, 0.00 v3.1.0 +% Syntax : Number of formulae : 4 ( 0 unit) +% Number of atoms : 8 ( 0 equality) +% Maximal formula depth : 5 ( 4 average) +% Number of connectives : 7 ( 3 ~ ; 0 |; 1 &) +% ( 1 <=>; 2 =>; 0 <=) +% ( 0 <~>; 0 ~|; 0 ~&) +% Number of predicates : 6 ( 0 propositional; 1-2 arity) +% Number of functors : 0 ( 0 constant; --- arity) +% Number of variables : 6 ( 0 singleton; 4 !; 2 ?) +% Maximal term depth : 1 ( 1 average) +% SPC : FOF_SAT_RFO_NEQ + +% Comments : Sean Bechhofer says there are some errors in the encoding of +% datatypes, so this problem may not be perfect. At least it's +% still representative of the type of reasoning required for OWL. +%------------------------------------------------------------------------------ +%----Thing and Nothing +fof(axiom_0,axiom, + ( ! [X] : + ( cowlThing(X) + & ~ cowlNothing(X) ) )). + +%----String and Integer disjoint +fof(axiom_1,axiom, + ( ! [X] : + ( xsd_string(X) + <=> ~ xsd_integer(X) ) )). + +%----Super cNothing +fof(axiom_2,axiom, + ( ! [X] : + ( cNothing(X) + => ~ ( ? [Y] : rp(X,Y) ) ) )). + +%----Super cNothing +fof(axiom_3,axiom, + ( ! [X] : + ( cNothing(X) + => ? [Y0] : rp(X,Y0) ) )). + +%------------------------------------------------------------------------------ -- cgit v1.2.3