%------------------------------------------------------------------------------ % File : SWB003+0 : TPTP v7.2.0. Released v5.2.0. % Domain : Semantic Web % Axioms : RDFS % Version : [Sch03] axioms : Especial. % English : % Refs : [Sch03] Schneider, M. (2011), Email to G. Sutcliffe % Source : [Sch03] % Names : axioms-rdfs-standard [Sch03] % Status : Satisfiable % Syntax : Number of formulae : 80 ( 62 unit) % Number of atoms : 108 ( 0 equality) % Maximal formula depth : 9 ( 2 average) % Number of connectives : 28 ( 0 ~; 0 |; 8 &) % ( 5 <=>; 15 =>; 0 <=; 0 <~>) % ( 0 ~|; 0 ~&) % Number of predicates : 6 ( 0 propositional; 1-3 arity) % Number of functors : 33 ( 33 constant; 0-0 arity) % Number of variables : 37 ( 0 sgn; 37 !; 0 ?) % Maximal term depth : 1 ( 1 average) % SPC : FOF_SAT_EPR % Comments : %------------------------------------------------------------------------------ %----I(s p o) = true -> I(p) in IP %----Note: the "iext" predicate seems to represent a true triple, %----not quite the IEXT mapping [CHECK!] fof(simple_iext_property,axiom,( ! [S,P,O] : ( iext(P,S,O) => ip(P) ) )). %----Set IR %----The set IR is the set of all resources. fof(simple_ir,axiom,( ! [X] : ir(X) )). %----Set LV %----The set LV of all data values is a subset of IR. fof(simple_lv,axiom,( ! [X] : ( lv(X) => ir(X) ) )). %----Axiomatic Triples for the Collection Vocabulary (Lists): rdf:first fof(rdf_collection_first_type,axiom,( iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property) )). %----Axiomatic Triples for the Collection Vocabulary (Lists): rdf:nil fof(rdf_collection_nil_type,axiom,( iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List) )). %----Axiomatic Triples for the Collection Vocabulary (Lists): rdf:rest fof(rdf_collection_rest_type,axiom,( iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property) )). %----Axiomatic Triples for the Container Vocabulary: rdf:_n fof(rdf_container_n_type_001,axiom,( iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property) )). %----Axiomatic Triples for the Container Vocabulary: rdf:_n fof(rdf_container_n_type_002,axiom,( iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property) )). %----Axiomatic Triples for the Container Vocabulary: rdf:_n fof(rdf_container_n_type_003,axiom,( iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property) )). %----Axiomatic Triples for the Reification Vocabulary: rdf:object fof(rdf_reification_object_type,axiom,( iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property) )). %----Axiomatic Triples for rdf:value-- fof(rdf_reification_predicate_type,axiom,( iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) )). %----Axiomatic Triples for the Reification Vocabulary: rdf:subject fof(rdf_reification_subject_type,axiom,( iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property) )). %----IP and rdf:Property fof(rdf_type_ip,axiom,( ! [P] : ( iext(uri_rdf_type,P,uri_rdf_Property) <=> ip(P) ) )). %----Axiomatic Triple for rdf:type fof(rdf_type_type,axiom,( iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property) )). %----Axiomatic Triple for rdf:type fof(rdf_value_type,axiom,( iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property) )). fof(rdfs_annotation_comment_domain,axiom,( iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource) )). fof(rdfs_annotation_comment_range,axiom,( iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal) )). fof(rdfs_annotation_isdefinedby_domain,axiom,( iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource) )). fof(rdfs_annotation_isdefinedby_range,axiom,( iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource) )). fof(rdfs_annotation_isdefinedby_sub,axiom,( iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso) )). fof(rdfs_annotation_label_domain,axiom,( iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource) )). fof(rdfs_annotation_label_range,axiom,( iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal) )). fof(rdfs_annotation_seealso_domain,axiom,( iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource) )). fof(rdfs_annotation_seealso_range,axiom,( iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource) )). %----Definition of ICEXT fof(rdfs_cext_def,axiom,( ! [X,C] : ( iext(uri_rdf_type,X,C) <=> icext(C,X) ) )). %----IC and rdfs:Resource fof(rdfs_class_instsub_resource,axiom,( ! [C] : ( ic(C) => iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource) ) )). %----IC and rdfs:Resource fof(rdfs_collection_first_domain,axiom,( iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List) )). %----IC and rdfs:Resource fof(rdfs_collection_first_range,axiom,( iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource) )). fof(rdfs_collection_rest_domain,axiom,( iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List) )). fof(rdfs_collection_rest_range,axiom,( iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List) )). fof(rdfs_container_alt_sub,axiom,( iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container) )). fof(rdfs_container_bag_sub,axiom,( iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container) )). %----rdfs:ContainerMembershipProperty fof(rdfs_container_containermembershipproperty_instsub_member,axiom,( ! [P] : ( icext(uri_rdfs_ContainerMembershipProperty,P) => iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member) ) )). fof(rdfs_container_containermembershipproperty_sub,axiom,( iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property) )). fof(rdfs_container_member_domain,axiom,( iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource) )). fof(rdfs_container_member_range,axiom,( iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource) )). fof(rdfs_container_n_domain_001,axiom,( iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource) )). fof(rdfs_container_n_domain_002,axiom,( iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource) )). fof(rdfs_container_n_domain_003,axiom,( iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource) )). fof(rdfs_container_n_range_001,axiom,( iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource) )). fof(rdfs_container_n_range_002,axiom,( iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource) )). fof(rdfs_container_n_range_003,axiom,( iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource) )). fof(rdfs_container_n_type_001,axiom,( iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) )). fof(rdfs_container_n_type_002,axiom,( iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) )). fof(rdfs_container_n_type_003,axiom,( iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) )). fof(rdfs_container_seq_sub,axiom,( iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container) )). fof(rdfs_dat_xmlliteral_sub,axiom,( iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal) )). %----type of rdf:XMLLiteral fof(rdfs_dat_xmlliteral_type,axiom,( iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype) )). %----rdfs:Datatype and rdfs:Literal fof(rdfs_datatype_instsub_literal,axiom,( ! [D] : ( icext(uri_rdfs_Datatype,D) => iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal) ) )). %----rdfs:Datatype is a sub class of rdfs:Class fof(rdfs_datatype_sub,axiom,( iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class) )). %----domain of rdfs:domain fof(rdfs_domain_domain,axiom,( iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property) )). %----Semantic Condition for rdfs:domain fof(rdfs_domain_main,axiom,( ! [P,C,X,Y] : ( ( iext(uri_rdfs_domain,P,C) & iext(P,X,Y) ) => icext(C,X) ) )). %----range of rdfs:domain fof(rdfs_domain_range,axiom,( iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class) )). %----Definition of set IC based on class extensions of rdfs:Class fof(rdfs_ic_def,axiom,( ! [X] : ( ic(X) <=> icext(uri_rdfs_Class,X) ) )). %----Definition of set IR based on class extensions of rdfs:Resource fof(rdfs_ir_def,axiom,( ! [X] : ( ir(X) <=> icext(uri_rdfs_Resource,X) ) )). %----Definition of set LV based on class extensions of rdfs:Literal fof(rdfs_lv_def,axiom,( ! [X] : ( lv(X) <=> icext(uri_rdfs_Literal,X) ) )). %----type of rdf:Property (derivable RDFS-valid triple) fof(rdfs_property_type,axiom,( iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class) )). %----domain of rdfs:range fof(rdfs_range_domain,axiom,( iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property) )). %----Semantic Condition for rdfs:range fof(rdfs_range_main,axiom,( ! [P,C,X,Y] : ( ( iext(uri_rdfs_range,P,C) & iext(P,X,Y) ) => icext(C,Y) ) )). %----range of rdfs:range fof(rdfs_range_range,axiom,( iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class) )). fof(rdfs_reification_object_domain,axiom,( iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement) )). fof(rdfs_reification_object_range,axiom,( iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource) )). fof(rdfs_reification_predicate_domain,axiom,( iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement) )). fof(rdfs_reification_predicate_range,axiom,( iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource) )). fof(rdfs_reification_subject_domain,axiom,( iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement) )). fof(rdfs_reification_subject_range,axiom,( iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource) )). %----domain of rdfs:subClassOf fof(rdfs_subclassof_domain,axiom,( iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class) )). %----Main Semantic Conditions for rdfs:subClassOf fof(rdfs_subclassof_main,axiom,( ! [C,D] : ( iext(uri_rdfs_subClassOf,C,D) => ( ic(C) & ic(D) & ! [X] : ( icext(C,X) => icext(D,X) ) ) ) )). %----range of rdfs:subClassOf fof(rdfs_subclassof_range,axiom,( iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class) )). %----Reflexivity of rdfs:subClassOf on IC fof(rdfs_subclassof_reflex,axiom,( ! [C] : ( ic(C) => iext(uri_rdfs_subClassOf,C,C) ) )). %----Transitivity of rdfs:subClassOf on IC fof(rdfs_subclassof_trans,axiom,( ! [C,D,E] : ( ( iext(uri_rdfs_subClassOf,C,D) & iext(uri_rdfs_subClassOf,D,E) ) => iext(uri_rdfs_subClassOf,C,E) ) )). %----domain of rdfs:subPropertyOf fof(rdfs_subpropertyof_domain,axiom,( iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property) )). %----Main Semantic Condition for rdfs:subPropertyOf fof(rdfs_subpropertyof_main,axiom,( ! [P,Q] : ( iext(uri_rdfs_subPropertyOf,P,Q) => ( ip(P) & ip(Q) & ! [X,Y] : ( iext(P,X,Y) => iext(Q,X,Y) ) ) ) )). %----range of rdfs:subPropertyOf fof(rdfs_subpropertyof_range,axiom,( iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property) )). %----Reflexivity of rdfs:subPropertyOf on IP fof(rdfs_subpropertyof_reflex,axiom,( ! [P] : ( ip(P) => iext(uri_rdfs_subPropertyOf,P,P) ) )). %----Transitivity of rdfs:subPropertyOf on IP fof(rdfs_subpropertyof_trans,axiom,( ! [P,Q,R] : ( ( iext(uri_rdfs_subPropertyOf,P,Q) & iext(uri_rdfs_subPropertyOf,Q,R) ) => iext(uri_rdfs_subPropertyOf,P,R) ) )). %----domain of rdf:type fof(rdfs_type_domain,axiom,( iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource) )). %----range of rdf:type fof(rdfs_type_range,axiom,( iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class) )). fof(rdfs_value_domain,axiom,( iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource) )). fof(rdfs_value_range,axiom,( iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource) )). %------------------------------------------------------------------------------