|From:||PATRICK BROWNE <patrick.browne@xxxxxx>|
|Date:||Wed, 16 Apr 2014 10:37:27 +0100|
I am interested in using Equational Theories (ET), Equational Logic (EL), and an algebraic specification language (CafeOBJ) 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, 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 ?
 CafeOBJ http://www.ldl.jaist.ac.jp/cafeobj/
 Formalising Ontologies and Their Relations,Trevor J. M. Bench-Capon, Grant Malcolm: cseweb.ucsd.edu/groups/tatami/seek/ontodb.ps
 Semantics for Interoperability: Trevor J. M. Bench-Capon, Grant Malcolm, Michael J. R. Shave: cgi.csc.liv.ac.uk/~grant/PS/ontos.ps
 Algebraic Semantics of Imperative Programs, by Joseph Goguen and Grant Malcolm, page 85, http://cseweb.ucsd.edu/~goguen/sys/objcourse.html
 An Executable Course in the Algebraic Semantics of Imperative Programs, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.7321
 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
_________________________________________________________________ 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>|
|Previous by Date:||[ontolog-forum] Two research fellow/assistant professor openings in Bozen-Bolzano, John F Sowa|
|Next by Date:||[ontolog-forum] Ontology based "Context Lenses" into Linked Open Data, Kingsley Idehen|
|Previous by Thread:||[ontolog-forum] Two research fellow/assistant professor openings in Bozen-Bolzano, John F Sowa|
|Next by Thread:||Re: [ontolog-forum] Equational Logic for Ontologies?, Obrst, Leo J.|
|Indexes:||[Date] [Thread] [Top] [All Lists]|