Comment by nisa | Hacker News Reader

Comment by nisa | Hacker News Reader

The whole topic of logic is largely absent at my University - can anyone recommend some literature or a path to follow?

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!

I'd start by learning Prolog. It is a border-line mystical experience. It took me a lot longer to understand Prolog and become effective in it than anything else I've learned, but nothing else has changed my perspective about problem solving more.

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.

https://github.com/simply-logical/simply-logical

Wow. Thank you. This is enough work for the next few months or years? I'll try to go that way.

I second the recommendation for 'Simply Logical'!

I recommend "Software Foundations" by Pierce and others https://softwarefoundations.cis.upenn.edu/ if you're a programming fan.

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.

Wow 6 volumes. Added to the list. German is also fine if there is literature and I'm trying to work on my math understanding. I also found some interesting papers that solve i.e. datalog using matrices with algebraic methods. https://arxiv.org/abs/1608.00139

Guess I'll start slowly and see how far I come. Thanks!

I share your wish that there were materials that more clearly mapped between these concepts. There's several implicated but separate concerns:

  - 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.)

Reply on news.ycombinator.com