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
|
_________________________________________________________________
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)
|