Chris P, Chris M, and Alex, There is no reason why you need to standardize on one specific notation for everybody. The ISO standard for Common Logic was designed with an ABSTRACT SYNTAX, which allows any number of concrete syntaxes, linear or diagrammatic. Since Python is a procedural language, I'm sure that some data-like subset of Python was used to represent the data model. Ideally, that subset should be designed to conform to the CL abstract syntax. In fact, the DOL standard by the Object Management Group supports translation among an open-ended variety of concrete syntaxes. To Alex: There is no need for you (or anybody else) to lean Python. With the DOL standard, any syntax that conforms to the ISO standard for Common Logic can be automatically translated to and from any syntax that can express FOL or many subsets and supersets of FOL. That includes OWL, Turtle, UML, and even TPTP (Thousands of Problems for Theorem Provers). I discussed those options in my ESWC slides, for a talk at the 2020 European Semantic Web Conference. See the references in slides 8 to 11 of https://jfsowa.com/talks/eswc.pdf Those four slides and the references they contain, answer the basic questions. But you can continue to read more slides and references for more background information. Bit remember that slides 8 to 11 are sufficient to support FOL. John _________________________________________ From: "Chris Partridge" <partridge.csj(a)gmail.com> @chris_mungall - apologies if you answered earlier, but what 'format' are you using to input the FOL axioms? TPTP? CLIF? (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.)On Fri, 11 Oct 2024 at 19:32, Chris Mungall <cjmungall(a)lbl.gov> wrote: 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(a)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...(a)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...(a)googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/ac5c66d7-6ea7-4554-9cad-507…. -- 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(a)googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/22a5fd29-f005-40f5-bcdd-202…. -- 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(a)googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAN9Aifs6%3Dqnga%3DH%3D0rw-… 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(a)googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAMWD8MrFo2LNNPa9f0fi6BegQK….