I have been working with ontologies (RDF/OWL) a lot of time, using mostly them as an engineer, because they permitted SPARQL and rules essencially.
It's only recently, this year, that I started to really pay attention to the theoretical grounding of OWL. This lead me to dive into the zoo of many Description Logic and their desirable or undesirable properties.
I think there is some serious issues in the multiplication of work on DL, which are almost never considered under the perspective of actual usefulness, of their ability to describe the specific structures that are at core of many domains (law, clinical science, computer science...).
Quite some of the theoretical work in DL and logic seems to formally study and prove property about language (DL are language) that nobody is speaking or will ever speak. This is quite salient when considering the very little number of working reasoners (which are covering only a small fragment of DL described formally).
It seems to me that, after the incredibly fecund periods that started with Frege, Russel, Tarski, Hilbert, Godel, Carnap... The theoretical work was somewhat considered to be done and less attention was focused on formal language for Domain Description.
On the other hand, questions related to problem solving (planner) became treated only as SAT problem needing optimisation. With almost no reference to first order logic and thus having poor link with DL.
Finally, on the third hand, modal logic, which has clearly deep link with first order logic (the square operator/diamond operator and the existential quantifier/universal quantifier in particular), has been abandoned by computer scientist and become, more or less explicitly, a field of philosophy.
I think this state of affairs isn't satisfying and that there is a work of conceptual clarification and of revision of the foundation of mathematics that would integrate these development.
To that end, something that does seem absolutely essential is to give each other an easy access to reasoners. By easy access, I don't mean a program written in some obscure language whose source must be compiled on a specific linux.
I mean an access to the reasoning service through a (loosely standardized) REST API. These service should be accompanied with websites giving relevant example of using the reaoner, with an "online playground".
I think this could be done for classic DL such as EL or SHOIQ but also for modal logic in it's various kind (epistemic, deontic), and that could also could be done for planification based on First Order Logic.
I'm currently cogitating about the engineering question that would raise from such a logical zoo, and about a grammar that would be usable for every reasoning problem description involving this kind of logic.
If you are interested by the question and/or have skills in modern full stack architecture and Dockerisation, I'd be interested to have your opinion about the current situtation and the feasability of such a logic zoo, which would be an useful tool for clarifying the domain.
I suggest that you make contact with the automated theorem proving communit. One starting point is the Wikipedia entry
https://en.wikipedia.org/wiki/Automated_theorem_proving
another is the long running series of Conferences on Automated DEduction (CADE)
https://www.cadeinc.org
Thank you for these pointers, it looks like the field of automated theorem proving group together many fields of logic.
I haven't seen much about modal logic though, neither about Situation calculus.
I started to read some of your works and I'm interested in the approach you're taking. I hope to have occasion to exchange with you in the future.
Your idea sounds very interesting and I would really like to play around with those reasoners (ideally based on some well documented examples). Maybe a good start would be to setup a repo and create a dockerfile for each reasoner which should be supported. Once those backends behave well-defined it should not be too hard to develop a frontend providing the REST-API.
Some time ago I did something loosly related: https://github.com/ackrep-org/ackrep_deployment.
Carsten Knoll Thank you for your response. I agree that a Docker based solution would be ideal.
I've been working with Portainer and Traefik in order to create back-end that where connected to a Docker instance using the subdomain to maintain the routing (ex. xxx.mydomain.eu -> docker_Instance_1:8000, yyy.mydomain.eu-> docker_Instance_2:70000). It's really convenient since launching a new service just requires a (free) cloudflare account and to give some correct parameters to the docker-compose file.
The question I'm not sure about is what would be the common language to use in order to communicate with reasoners. Description logic based reasoners are frequently based on OWL-API (https://www.w3.org/2001/sw/wiki/OWL/Implementations) but I could not really find something similar for modal logic reasoners. For situation calculus the standard seems to be GOLOG which is based on Prolog. I wonder what would be the format that could ease the expression of logic problems into different serialization accepted by reasoners. N3 seems to be a good candidate as far as I can tell, but only for DL not for modal logic.
I also can recommend Traefik see e.g., https://github.com/ackrep-org/ackrep_deployment/blob/main/docker-compose.yml
I use it simply with some registered domain without any cloudflare involved.
While I have some experiences with reasoning over description logics, this is (up to now) not true for modal logic. Maybe one way would be to precisely define a minimal example problem in natural language and ask a stackoverflow question how this could best be represented in a machine-actionable way.
(I think due to the network effect stackoverflow has a higher chance to yield a useful answer on a precise question).
I'm coming back to to that question after some time and various research focused on reasoners with open sources (and backed by research papers).
These reasoners generally share a base ground :
- a syntax for statements (ex. Triple, predication over atoms, like women(a) in prolog
- a way to express binary relations (objectPropeties in rdf, spouse (mary,a) in prolog
- a way to express n-ary relations (possible yet unpractical in rdf contrary to prolog)
- a way to evaluate if there is at least one theory (a conjunction of formula that may include variables provided the quantification over these make sense) which evaluate to true over the knowledge base
(I'll finish this later because my phone rings)
- Badges
- Science topic
- Similar topics
- Mathematics