Explore tooling to support some use of first-order logic in COB

[jamesaoverton]

I would really like to be able to add FOL axioms to cob-edit.owl. Even if we can't use them in OWL, it could express our intent more clearly, and we could try to find tools to check some things.

Let's use this issue to discuss that.

[jamesaoverton]

IAO already includes a few annotation properties to keeping track of FOL axioms, which are used in BFO:

• IAO:0000602 has associated axiom(fol)
• IAO:0000601 has associated axiom(nl)
• IAO:0010000 has axiom label

[jamesaoverton]

What I would really like is to be able to express FOL axiom in some formal language, and then run multiple different FOL reasoners / provers over the axioms. There are some directions that seem promising to me, but that I've never been able to properly follow up on:

1. HETS http://www.hets.eu
2. TPTP format http://www.tptp.org/TPTP/Proposals/LogicSpecification.html
3. Alan Ruttenberg built some tools for using multiple provers on BFO for the ISO process, but I believe this is not public
4. I think ISO Common Logic should be able to do this -- are there tools?

Of course, there's a range of specific provers and proof systems, e.g. Isabelle, Cog, E Theorem Prover. Maybe supporting just one of these is good enough.

[jannahastings]

@fabianneuhaus and I will give an example of OWL+FOL working together in DOL + Hets.

(Hets is compatible with different FOL provers -- I use E prover -- and different syntaxes, including TPTP.)

[alanruttenberg]

The ones in BFO are old and from a mistaken understanding, developed by a visiting student IIRC. They aren't present in BFO 2020.

I haven't yet augmented BFO 2020 with the current axioms, but plan to at some point. However the axioms are publically posted now.

I agree that we should be including axioms where possible. One issue is that that the axioms don't always separate neatly by term, as they do for the most part ink OWL. Analogous to GCIs, where protege arranges to show GCIs on terms that are referenced, even though they aren't directly attached to any one term. So some thought needs to put into how they are organized and to what the process is to deploy them for reasoning tasks.

To the extent you are, or become, interested in adding such functionality to ROBOT, I can work with you to explain the tooling I've been using.

I'm sorry I wasn't able to attend the COB meeting. Family health issues have been occupying my full time. I'm hoping to contribute to COB more as they resolve.

Alan

On Monday, August 31, 2020, James A. Overton [email protected] wrote:

IAO already includes a few annotation properties to keeping track of FOL axioms, which are used in BFO:

IAO:0000602 has associated axiom(fol) IAO:0000601 has associated axiom(nl) IAO:0010000 has axiom label

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[fabianneuhaus]

Here is a small example for combining OWL with FOL in DOL:

https://www.omg.org/spec/DOL/About-DOL/

Let's first define a simple parthood ontology in OWL:

logic OWL ontology Parthood_OWL = ObjectProperty: isPartOf ObjectProperty: isProperPartOf Characteristics: Asymmetric SubPropertyOf: isPartOf end

The first line in sets the language. The keyword ontology tells DOL that a new ontology is defined. The stuff behind the "=" is ordinary Manchester syntax closing with "end" Alternatively, one could just store the whole ontology somewhere else in a normal owl file and define

ontology Parthood_OWL = <some_IRI>

Because of OWL DL's limitation we cannot axiomatise an object property to be both asymmetric and transitive in OWL.

Thus, we can build the ontology that is an extension of the OWL ontology in Common Logic in DOL. This is used by first translating the OWL ontology to Common Logic and then adding a new axiom with "then".

logic CommonLogic ontology Parthood_CL = Parthood_OWL with translation OWL22CommonLogic
then (forall (x y z) (if (and (isProperPartOf x y) (isProperPartOf y z)) (isProperPartOf x z))) end

A running example is here http://rest.hets.eu (choose minimal example -> DOL -> submit) If you click on the green bubbles you can inspect the extended CL theory. One problem is that currently our OWL to CL translation is too verbose. We are planning to have a student improve on that next semester

If you don't like Common Logic, it also works with CASL (another FOL dialect).

[fabianneuhaus]

In case you want to use TPTP as the FOL-dialect it works similarly but with the additional quirk that there is no direct translation currently implemented in Hets. Thus, one needs to translate first from OWL to CASL and then from CASL to TPTP. The following defines first an OWL ontology O1, then a TPTP ontology O2 and lastly an ontology O3 that is the result of translating O1 from OWL to TPTP via CASL, and adding the axioms from O3. As previously mentioned O1 and O2 don't need to be defined locally in the file, one can use IRIs to identify some ontology on the web.

logic OWL ontology O1 = Class: man Class: mortal end

logic TPTP ontology O2 = fof(ax1, axiom, (![X]: (man(X) => mortal(X)) )). end

ontology O3 = O1 with translation OWL22CASL with translation CASL2TPTP_FOF then O2 end

[fabianneuhaus]

Here is a more realistic example based on Chris’s comment: https://github.com/OBOFoundry/COB/pull/118/files#diff-8ab72ddbbc7625da75e536c31ccc4c28

%% Atom: A material entity consisting of exactly one atomic nucleus and the electron(s) orbiting it.

logic OWL 

ontology MaterialEntity_DL  = 

	ObjectProperty: part_of 
	ObjectProperty: has_part 
		InverseOf: part_of 

	Class: MaterialEntity 
	Class: Atom 
		SubClassOf: has_part exactly 1 Nucleus 
		SubClassOf: has_part some Electron 
	 
	Class: Nucleus 	
	Class: Electron 
end 

%% The OWL ontology is missing the fact that electrons orbit around their atoms. 
%% We can do that in CL by extending the original ontology. 

logic CommonLogic 
ontology MaterialEntity_CL  = 
	MaterialEntity_DL with translation OWL22CommonLogic 
	then 
	
	(forall (x y)
		(if
			(and 
				(Atom x) (Electron y) (part_of y x)
			)
			(orbits y x)	
		)
	)
end 


%% Molecular Entity: A material entity that consists of two or more atoms that are all connected via covalent bonds such that any atom can be transitively connected with any other atom.

logic OWL 

ontology MolecularEntity_DL = 
	MaterialEntity_DL then 

	ObjectProperty: connectedByCovalentBond 
		Domain: Atom
		Range: Atom  
		Characteristics: Irreflexive, Symmetric 
		
	Class: MolecularEntity  	
		SubClassOf: MaterialEntity 
		SubClassOf: has_part min 2 Atom 
end 

%% We haven't represented that the atoms in a molecule are connected. Switching back to CL. 


logic CommonLogic 

%% The following ontology is just defines an auxiliary predicate CovalentBondChain 
%%  which is an n-ary predicate that identifies a path through a molecule along the covalent bond.  
%% This is needed to axiomatize that the atoms of a molecule are connected. 
%% Note that this is using sequence variables which are a feature of CL that exceed plain FOL 

ontology CovalentBondChain = 

	(not (CovalentBondChain) ) 	
	(forall (x) (not  (CovalentBondChain x) ))
	
	(forall (x y)
		(iff (connectedByCovalentBond x y) (CovalentBondChain x y) )	
	)

	(forall (x y ...)
		(iff (and (connectedByCovalentBond x y) (CovalentBondChain y ...))  
			(CovalentBondChain x ... )
		)	
	)
end 

%% The following ontology defines the ontology MolecularEntity_CL, where the MaterialEntity_CL ontology is extended by the content from the MolecularEntity_DL ontology and our auxiliary ontology and an additional axiom, which guarantees that two atoms in a molecule can be connected via a covalent bond chain. 


ontology MolecularEntity_CL = 
	MolecularEntity_DL with translation OWL22CommonLogic 
	and MaterialEntity_CL 
	and CovalentBondChain 
	then 

	(forall (x y z)
		(if 
			(and (MolecularEntity x) (Atom y) (Atom y) (part_of y x ) (part_of z x)
			)
			(exists (...) (CovalentBondChain y ... z)
			)
		)
	)

[fabianneuhaus]

If you run the previous example through Hets, you get the following graph that shows the interaction between the various ontology modules. The normal arrows indicate extensions. The double arrows represent translations. The green nodes without labels are unnamed ontologies.

[jamesaoverton]

Thanks @fabianneuhaus! I'll play with this as soon as I get a chance. Much appreciated.