How are axiomatic theories represented?

[ChristophB]

Finally, there are a lot of axioms listed in some papers, like the one above or BAUMANN, Ringo; LOEBE, Frank; HERRE, Heinrich. Axiomatic theories of the ontology of time in GFO. Applied Ontology, 2014, 9. Jg., Nr. 3-4, S. 171-215. Are they only represented as a OWL class or is there a plain list of these axioms/FOL-theory somewhere?

[k00ni]

I would like to shed some light here. Is the publication (e.g. in a text file or in the TPTP format) of a raw list of axioms used in many GFO publications even in the interest of the research group? Having such a list would enable further use cases, such as using Vampire to run further analysis, evaluation etc.

[k00ni]

What do you suggest when I want to work with GFO axioms written in DL/FOL as well as the OWL ontology (base
or light)? It seems that these are kept in two separate worlds even though they share at least the same GFO terms/concepts. GFO axioms are only presented in publications as far as I know. Are they managed somewhere else online or do they only exist in long Word-files locally on some computer?

Would it make sense to you to "port" them into the OWL ontology in some way so there is one single point of truth?

Benefits might be:

• one point to manage all of them instead of many
• easier way to synchronize them with the OWL ontology
• more consistent versioning possible because they are all in one place

Here is a rough example how to implement it in OWL using the TPTP format for FOL/DS formulas:

:MaterialContinuant 
  tptp:formula 
    "fof (foobar, axiom, ! [X]: MaterialContinuant(X) => MaterialObject(X) | MaterialAggregate(X) | MaterialPart(X))." .

One could write a program to read all GFO axioms, create a temp file and feed it to a theorem prover such as Vampire to run some checks.

[ChristophB]

@Onto-Med/gfo-developer

[k00ni]

What do you mean with @Onto-Med/gfo-developer?

[ChristophB]

What do you mean with @Onto-Med/gfo-developer?

To make sure they don't miss your question, I've pinged the GFO developers.

[k00ni]

I've started to play around with just 4 GFO axioms in TPTP + Vampire (https://github.com/vprover/vampire).

In the following a summary, but you can find my test code here: https://github.com/k00ni/GFO/tree/feature/axiom-list (e.g. axioms.p). Build the docker container by running make in the docker folder and then run the Vampire command below.

---

The 4 GFO axioms are:

∃x(Set(x)) ∧ ¬∃x(Set(x) ∧ Item(x))

Set(x) ∧ Set(y) → (x = y ↔ ∀u(u ∈ x ↔ u ∈ y))

∀xy(Item(x) ∧ Item(y) → ∃z(Set(z) ∧ z = {x, y}) 

∃x(Set(x) ∧ ∀u(u ∈ x ↔ Item(u))

(Source: General Formal Ontology (GFO) Part I: Basic Principles (2006), https://www.onto-med.de/sites/www.onto-med.de/files/files/uploads/Publications/2006/om-report-no8.pdf)

Here is the TPTP version of these axioms:

%
% Sources
% [1] - General Formal Ontology (GFO)  Part I: Basic Principles (2006),
%       https://www.onto-med.de/sites/www.onto-med.de/files/files/uploads/Publications/2006/om-report-no8.pdf
%

% ∃x(Set(x)) ∧ ¬∃x(Set(x) ∧ Item(x))
% Source: [1], page 18
fof(a1, axiom, ( ? [X] : set(X) & ~ ? [X] : ( set(X) & item(X) ) )).

% Set(x) ∧ Set(y) → (x = y ↔ ∀u(u ∈ x ↔ u ∈ y))
% Source: [1], page 18
fof(a2, axiom, ( set(X) & set(Y) => ( X = Y <=> ![U]:( member(U,X) <=> member(U,Y) )))).

% ∀xy(Item(x) ∧ Item(y) → ∃z(Set(z) ∧ z = {x, y}))
% Source: [1], page 18
fof(a3, axiom, ![X,Y]:( item(X) & item(Y) => ?[Z]: ( set(Z) & ![U]:( member(U, Z) <=> (U = X | U = Y ))))).

% ∃x(Set(x) ∧ ∀u(u ∈ x ↔ Item(u)))
% Source: [1], page 18
fof(a4, axiom, ?[X]:( set(X) & ![U]: (member(U,X) <=> item(U)) )).

For axiom a1-a3 Vampire (v4.9) is very fast (0.003 s) and returns "Satisfiable".
But with a4 it runs for max time and returns "Refutation not found, non-redundant clauses discarded". It might return "Satisfiable" for a way higher time value, but I didn't try. I am sincerely hope I made a mistake somewhere.

Here is the whole Vampire call:

vampire -t 600 axioms.p

% Running in auto input_syntax mode. Trying TPTP
% Refutation not found, non-redundant clauses discarded%
------------------------------
% Version: Vampire 4.9 (commit 5ad494e78 on 2024-06-14 14:05:27 +0100)
% Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3
z3-4.8.4-7980-g79bbbf76d
% Termination reason: Refutation not found, non-redundant clauses
discarded
% Memory used [KB]: 9020855
% Time elapsed: 500.836 s

Vampire seems to be very fast (by their own words), but if it already takes so much time just for 4 axioms, how much does it need for all the others?

This leads to the question if and how the GFO developers evaluate their own FOL-formulas?

[k00ni]

Small update: I tried it with SMT-Lib's Z3 and got it to return "sat" (satisfiable).

SMT-code is new to me, so I generated it using Copilot. After a few rounds of trial and error I got the following. At first glance it seems to be a correct "translation" of the four axioms from above.

(set-logic AUFLIA)

; Definitionen für set, item, member
(declare-fun set (Int) Bool)
(declare-fun item (Int) Bool)
(declare-fun member (Int Int) Bool)

; Axiom 1: ∃x(set(x)) ∧ ¬∃x(set(x) ∧ item(x))
(assert (and (exists ((x Int)) (set x))
(not (exists ((x Int)) (and (set x) (item x))))))

; Axiom 2: set(x) ∧ set(y) → (x = y ↔ ∀u(member(u, x) ↔ member(u, y)))
(assert (forall ((x Int) (y Int))
(or (not (and (set x) (set y)))
(and (= x y) (forall ((u Int)) (= (member u x) (member u y)))))))

; Axiom 3: ∀x y(item(x) ∧ item(y) → ∃z(set(z) ∧ ∀u(member(u, z) ↔ (u = x ∨ u = y))))
(assert (forall ((x Int) (y Int))
(or (not (and (item x) (item y)))
(exists ((z Int)) (and (set z) (forall ((u Int)) (= (member u z) (or (= u x) (= u y)))))))))

; Axiom 4: ∃x(set(x) ∧ ∀u(member(u, x) ↔ item(u)))
(assert (exists ((x Int))
(and (set x)
(forall ((u Int)) (= (member u x) (item u))))))

(check-sat)

(Code can be found here: https://github.com/k00ni/GFO/blob/feature/axiom-list/axioms.smt2)

So maybe Z3 is to be preferred in this regard instead of Vampire.

[MichaelRawson]

Hi @k00ni - there's nothing wrong with your axioms that I can see (although we may be able to optimise - see later), but what you are asking Vampire to do is "check their consistency by trying to derive falsum" - which Vampire will try very hard to do (try --show_active on to see a subset of what it's up to), but ultimately this is not very easy for it. These axioms are not contradictory, so it does not succeed - the only way it could detect this is by saturating, "running out of things to do" - which it manages somewhat heroically with axioms 1-3, but not with 4.

What you likely want to do is to prove some conjecture from these axioms, which Vampire will find much faster.

If you really want to check their consistency, try the finite model builder: vampire -sa fmb finds a finite model of size 1 immediately. This works if one can construct a finite set of objects satisfying these axioms. Z3 works differently again to these modes: indeed you can and should try multiple systems.

---

A side note about your axioms.

TPTP supports a typed language, and your set and item predicates look a lot like type guards to me. I could imagine that either (i) sets can only contain items and not other sets, (ii) sets are stratified into sets of items, sets of sets of items, and so on, or (iii) you really want mixed sets of arbitrary nesting. If (i) or (ii) then we can do much better with the type system, (iii) I don't see how to do much better.

[floebe]

I apologize for the extreme delay in responding and for responding briefly and likely unsatisfactorily, also with high chances that a follow-up takes much time again. :-( That said:

[@k00ni] [...] Is the publication (e.g. in a text file or in the TPTP format) of a raw list of axioms used in many GFO publications even in the interest of the research group?

In principle and in theory, yes and "Sure!". :-) In practice, it usually doesn't make it to the top-priority, due to limited time available. :-(((

Having such a list would enable further use cases, such as using Vampire to run further analysis, evaluation etc.

I fully agree and it'd be great to do "that" on the one hand, where "that" should be further specified and brought into a reasonable order. On the other hand, pursuing "that" may require a very substantial amount of time. I myself am highly constrained, as much as I regret that.

---

Regarding what is available yet:
The most elaborate file(s?) we had produced (locally) was/is a version of the first-order time theory, at that time (around 2009/10?) in .dfg format used by SPASS, which could be translated to .tptp.

If that'd be of interest for experiments, I may try finding it.

---

A side comment on the formats:
In the long run and for sharing purposes, what I'd find most attractive so far would be to aim at (CommonLogic) CLIF representations of the first-order formulas and modules, as practiced by M. Gruninger in his COLORE repository.
That said, at least I myself lack tool support to convert CLIF easily to tptp or other formats that provers may digest well.