(The reason I'm asking is we did some work a while ago and we found it useful to have a more human-readable input format - we went with CLIF using an EBNF grammar approach to read - converted to an internal model then output in whatever format needed - often TPTP for e.g. Vampire. One of the design questions that came up was what was the best way to consume (effectively unstructured) text FOL 9e.g. a csv) at scale - and then what a common data structure that could output a variety of formats would look like.)

Thanks Alex!

To be clear, the reasoning is typically not done in Python. Python acts as the glue. Many developers use Python to specify data-models, but these data models are usually accompanied by complex procedural code for both validation and inference. The idea is to use Python syntax to encode FOL axioms for these data models (not dissimilar to using OCL with UML, or a rules language alongside Frames), and then to seamlessly run reasoners/solvers directly from Python (although these are carried out by integrations, e.g. clingo, souffle, Prover9, Z3).

I chose the paths/graphs examples because it's familiar to both ordinary developers and is a staple of datalog documentation, but of course more sophisticated theories are possible.

On Fri, Oct 11, 2024 at 1:53 AM alex.shkotin <alex.shkotin@gmail.com> wrote:

Chris,

Never heard that reasoning can be done in Python. Too bad I don't know Python. I'll do it and make a line for it in the ugraph theory framework when I get to paths. Path has a rather subtle definition. And path is an entity on its own where your Path is actually a predicate of path existence.

And following [GNaA] 1.3 we have to define "walk" first,  then "trail", and then "path" as a property of sequence of vertices and nodes.

And your two axioms 

are theorems in ugraph theory.

We have a polymorphic predicate adjacent where you use Link. With definition:

rus

Пусть v1, v2 - две вершины. v1 смежна v2 еите v1 и v2 являются различными и концевыми вершинами некоторого ребра.

eng

Let v1, v2 be two vertices. v1 is adjacent to v2 iff v1 and v2 are distinct end vertices of some edge.

yfl

declaration adjacent func(TV vertex vertex) (v1 v2) ≝ (v1≠v2) & (∃e:edge(U) enp(v1 e) and enp(v2 e)).

Calculation on the model of logical formulas is clear to me. Especially if we specify how to encode quantifiers, but I'll definitely look at reasoning.

Very interesting!

Alex

[GNaA] Graphs, Networks, and Algorithms. M. N. S. Swamy, K. Thulasiraman. Wiley, 1981.

четверг, 10 октября 2024 г. в 04:40:01 UTC+3, Chris Mungall:

Most developers these days are familiar with Python. I have been tinkering with an approach that allows existing Python data models (expressed using pydantic, sqlmodel, sqlalchemy, or linkml) to be enhanced with arbitrary FOL axioms. There are integrations with FOL solvers, and also with datalog and ASP engines (for programs that have the requisite expressivity), and soon OWL reasoners. There is also some preliminary LLM integration too.

Comments welcome:

https://py-typedlogic.github.io/

On Wed, Oct 9, 2024 at 12:42 AM 'Knowledge representation' via ontolog-forum <ontolo...@googlegroups.com> wrote:

What user-friendly* tools capable of handling full first-order logic do you know?

What tools can you build a conceptual model, ontology in FOL?

What is a stack for: translating natural language sentences into FOL and then FOL to a computable language?

If you refer to a particular FOL computable language, such as KIF, CL, or otherwise, what tools can easily help make an ontology formalized in the given langauge?

(for all questions: in an ontology-neutral way = without committing to any ontology. So no tools that force the user to use the terms of some ontology)

*For non-technical / non-computer scientists.

Thanks

--

All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/ac5c66d7-6ea7-4554-9cad-50777f899bd4n%40googlegroups.com.

--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/22a5fd29-f005-40f5-bcdd-2024b3f7b0ban%40googlegroups.com.

--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAN9Aifs6%3Dqnga%3DH%3D0rw-9J7rnCv_Rp9WRx-K2xwxxVAZcBSyQQ%40mail.gmail.com.

--All contributions to this forum are covered by an open-source license.For information about the wiki, the license, and how to subscribe or