Re: [ontolog-forum] Equational Logic for Ontologies?

[PATRICK BROWNE <patrick.browne@xxxxxx>]

Leo,
Thanks for you interest in my research.
I am aware and inspired by the work of Till Mossakowski and the CASL team[1].
Both CASL and CafeOBJ are based on the the theory of institutions.
They afford similar modularity features, but they are based on different logics.
CASL is based on first-order logic and is not directly executable and cannot be used for prototyping.
I wish to use the equational language of CafeOBJ for prototyping and also to simulate FOPL for reasoning about ontologies.
It seems that the work of Futatsugi and CafeOBJ team on "proof scores" comes nearest to my requirement[2,3].
I am unaware of any formal work on the relationship between equational proof scores and reasoning over FOPL

I was unaware of work of Hassan Ait-Kaci and will study his work.
Best Regards,
Pat

[1] Specification of ontologies in CASL : Klaus Luttich, Till Mossakowski
[2] Verifying Design with Proof Scores Kokichi Futatsugi, Joseph A. Goguen, and Kazuhiro Ogata
[3] Fostering Proof Scores in CafeOBJ, Kokichi Futatsugi

On 16 April 2014 13:51, Obrst, Leo J. <lobrst@xxxxxxxxx> wrote:

Hi, Pat,

 

You might look at Till Mossakowski’s Common Algebraic Specification Language (CASL) and related work, based on institutions: http://iws.cs.uni-magdeburg.de/~mossakow/.

 

Also, Hassan Ait-Kaci has done work in equational logics, multi-paradigm languages: http://www.hassan-ait-kaci.net/.

 

See also the following, which uses CASL:

Kutz, Oliver and Till Mossakowski. 2011. A Modular Consistency Proof for DOLCE. In Twenty-Fifth Conference on Artificial Intelligence (AAAI-11), held in San Francisco, California, August 7-11, 2011. http://www.informatik.uni-bremen.de/~okutz/AAAI11-Dolce.pdf.

 

Till, Hassan, and Oliver are members of the Ontolog Forum, so perhaps they will respond.

 

Thanks,

Leo

 

From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx] On Behalf Of PATRICK BROWNE
Sent: Wednesday, April 16, 2014 5:37 AM
To: ontolog-forum@xxxxxxxxxxxxxxxx
Subject: [ontolog-forum] Equational Logic for Ontologies?

 

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,
Pat
[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=10.1.1.13.7321
[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

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)