[Top] [All Lists]

[ontolog-forum] Equational Logic for Ontologies?

To: ontolog-forum@xxxxxxxxxxxxxxxx
From: PATRICK BROWNE <patrick.browne@xxxxxx>
Date: Wed, 16 Apr 2014 10:37:27 +0100
Message-id: <CAGFLrKfa-VWP4iL7u62GXUZ+p6UJEUZi_pgAg2nKaLyUWfnCYQ@xxxxxxxxxxxxxx>
Dear Forum.
I am interested in using Equational Theories (ET), Equational Logic (EL), and an algebraic specification language (CafeOBJ[1]) to represent and prototype ontologies.
We consider ET+EL+CafeOBJ as providing a "standard algebraic semantics".
The idea of using algebraic specification languages to represent ontologies is not new see [2,3].
I am aware that First Order Predicate Logic (FOPL) is the accepted standard for representing ontologies.
EL is regarded as a sub-logic of FOPL and any valid EL theorem is a valid FOPL theorem (but not vice versa).
The hoped for advantage is that algebraic semantics allows us to construct prototypes in the same software environment in which the ontology exists.
I wish to use *loose theories* in the framework of ET+EL+CafeOBJ to represent and prove sentences in First Order Predicate Logic (FOPL) for upper ontologies.
It is hoped that such an approach would help one to prove the consistency of axioms at upper-ontology level and permit one to relate these axioms to initial models (prototypes).

We follow Goguen and Malcolm's[2,3] guidelines for formulating FOPL sentences in the context of algebraic semantics.
These guidelines can be summarized as follows:
1)Translate first order sentences into sequences of declarations and reduction.
2)Predicates are represented as Bool valued operations.
3)Assumptions are represented by constants or equations.
4)Goals are reductions in the context of a theory plus the assumptions.
5)Universal quantifiers in goals are handled by introducing new constants.
6)Existential quantifiers in assumptions are handled by introducing Skolem functions.

I have have attempted to formulate FOPL axioms to algebraic semantics[6], but I do not have any theoretical basis for this.
I am unsure if this approach is theoretically sound.

My question is this:
Are there FOPL sentences that cannot be represented using "standard algebraic semantics"? (in this case ET+EL+CafeOBJ).
In other words is it possible to use equational axioms in an algebraic specification language to represent ontologies?
Note, I do not require that the equational axioms should be executable in the strict rewriting sense.
CafeOBJ provides a form of semi-automatic proof using selective bi-directional rewriting. Basically the user directs the proof.

Would anyone on this list be interested in addressing a more detailed version of this question that I posted to Theoretical Computer Science Stack Exchange [6]?

Best Regards,
[1] CafeOBJ http://www.ldl.jaist.ac.jp/cafeobj/
[2] Formalising Ontologies and Their Relations,Trevor J. M. Bench-Capon, Grant Malcolm: cseweb.ucsd.edu/groups/tatami/seek/ontodb.ps
[3] Semantics for Interoperability:  Trevor J. M. Bench-Capon, Grant Malcolm, Michael J. R. Shave: cgi.csc.liv.ac.uk/~grant/PS/ontos.ps
[4] Algebraic Semantics of Imperative Programs, by Joseph Goguen and Grant Malcolm, page 85, http://cseweb.ucsd.edu/~goguen/sys/objcourse.html
[5] An Executable Course in the Algebraic Semantics of Imperative Programs, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=
[6] Equational Logic and First Order Predicate Logic, http://cstheory.stackexchange.com/questions/22113/equational-logic-and-first-order-predicate-logic

This email originated from DIT. If you received this email in error, please delete it from your system. Please note that if you are not the named addressee, disclosing, copying, distributing or taking any action based on the contents of this email or attachments is prohibited. www.dit.ie

Is ó ITBÁC a tháinig an ríomhphost seo. Má fuair tú an ríomhphost seo trí earráid, scrios de do chóras é le do thoil. Tabhair ar aird, mura tú an seolaí ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon chóipeáil, aon dáileadh nó ar aon ghníomh a dhéanfar bunaithe ar an ábhar atá sa ríomhphost nó sna hiatáin seo. www.dit.ie

Tá ITBÁC ag aistriú go Gráinseach Ghormáin – DIT is on the move to Grangegorman

Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J    (01)

<Prev in Thread] Current Thread [Next in Thread>