Does there exist a system, e.g., software, an environment, a programming language, or the like, to represent knowledge and to reason with it, to query with, where the (descriptive) language used is at least predicate logic with modal operators, using standard logical symbols (⊃, ≡, ◇, ∧, etc.)? It has to follow the rules and practices of standard logic that have already been established. It must also have the capacity to quickly spit out a desktop application that can be used to query the knowledge database easily.

My interest at this point is especially experimental and personal. I have not yet come across anything in the software world that is what I seek.

What I have come across so far, are for example:

  • Prolog. I have used it before (some years ago) and I find its syntax (with symbols unlike what I seek) not suitable (and ugly) and, as far as I know, there are no modality operators.
  • Other logic-based programming languages. Most of them seem to imitate Prolog or are not in use or maintained, or lack what I seek, and so on.
  • Multi-paradigm programming languages including logic-based paradigm. Seems to be overkill for me, for I have no need of such a full-blown programming language. Even if I were to only use the parts for my purposes, then it still does not look as though it is a match to me: they do not use standard logical symbols, for example.
  • OWL and the like. This seems to be closer to what I seek, but it seems as though it is fairly new or not much used (at least relatively). (This might not be a problem.) It seems difficult to make choices in this case, as it seems that in my quest I have not simple direct answers. In this case I also have found applications such as Fluent Editor and Protégé. I would appreciate any relevant knowledge on this, their strengths and weaknesses, a comparison, and so on. Can they be used totally offline? And is OWL2 (or whatever usable syntax (Manchester, etc.)), e.g, sufficiently expressive to represent any knowledge a human might think of using, e.g, predicate and modal logic and even extra operators for greater expression? From what it looks like so far, the whole thing uses some descriptive logical language in-between propositional logic and predicate logic (so it is not standard in the sense that I mean). Furthermore, Fluent Editor seems to use a kind of subset of English as their language, which is perhaps nice, though I still prefer something that looks more like what I described earlier.

And is there some system where one could even assign one's own operators to replace the default ones?

So far only Fluent Editor and Protégé with some sort of OWL nature seem to be the best candidates. Can they be used offline and can they compile desktop query applications?

You can understand that I am in this quest not satisfied. It has been a search without sufficient result, and so somewhat frustrating. Is my quest in vain? Must I create the system I seek myself?

  • $\begingroup$ Software/tool recommendations are off-topic here. Your requirements are not clear to me ("to represent knowledge and to reason with it" is a very broad statement that could mean many possible things). Are you asking for something that can check the validity of statements in first-order logic? $\endgroup$
    – D.W.
    Mar 3 '19 at 19:45
  • $\begingroup$ Oh. I thought I was sufficiently clear in the first paragraph, especially combined with the bullet point "OWL and the like" and what came after it. Basically at this moment: I want an OWL editor like Fluent Editor, but with standard logical symbols (predicate logic at least) (including modality and whatnot), or even that I can include my own symbols. $\endgroup$
    – user101144
    Mar 7 '19 at 21:06
  • $\begingroup$ OK. Sounds like you're looking for a software product or tool. I'm afraid those requests are off-topic here. Sorry. You could try Software Recommendations Stack Exchange, but make sure to read their FAQ and software quality criteria before asking there. $\endgroup$
    – D.W.
    Mar 7 '19 at 21:10
  • $\begingroup$ Okay. Thanks for the tip. Sorry for the burden. $\endgroup$
    – user101144
    Mar 8 '19 at 19:48