If you're also into math, it's a beauty in itself (Godel's incompleteness theorem, quantifier elimination for logic formulas about complex numbers). I think there should be a good book on math logic somewhere, but I'm not familiar with books in English.
Guess I'll start slowly and see how far I come. Thanks!
Check out "Simply Logic" -- free ebook. It'll give you an intro into first order predicate logic and Prolog simultaneously.
I'd suggest solving AoC2023 puzzles in Prolog. It'll give you a decent coverage of the language and some of its advanced features.
- A syntax for expressing data or rules
- A semantics for data
- A semantics for logic (e.g. a logical formalization)
- A specific set of logical axioms & rules
- An algorithm for executing a logic program
- A storage system for facts/data
- A query system for facts/data
Most of the things you mention are a bundling of some or all of the above concepts. This makes sense because it's easier to provide working implementations that way.Some systems offer a limited amount of pluggability or alternative implementations for the same concept (e.g, different "solvers" for OWL.)
But I find that there's a pronounced lack of shared formalisms (or even shared knowledge) even around things that logically should be pretty convergent. Especially if they come from different domains originally (logic programming vs. theorem proving vs. constraint programming vs. database theory, for example.)
I'd like to understand the relationship to RDF / SHACL / OWL and Datalog - additionally what about first order logic with relations like it's used in model checkers like smtlib and temporal logics?
Could I build a system based on miniKaren that implements RDF and OWL? Can I do that with Datalog (i.e. cozodb?)
How would you implement something like validation / SHACL with a logic language? Datamotic / XTDB seem to use some idea like a record and offer bitemporality - is this somehwere in the literature described on a theoretical level?
How is the relationship to Hoare-Logic (we had a brief stunt into that for prooving correctness for loops)
Is it a feasable idea to implement something like Apache Jena in a Datalog database like cozodb or is it a conceptually a fools errand?
I only find very theory heavy works and venture capital backed websites that implement some part but I'm missing the bigger picture.
How to make a fast implementation would also be interesting. I just don't seem to see the forest for the trees.
I'm thankful for any hints!