Nate Cull (.social)Hmm, Rulelog.
I *really* hope this is not the best synthesis of logic to date. It looks kinda... hairy.
How did we get from
0 = false
1 = true
to
Skolemize the monotonadic varptor function of the pre-literal dynastic modifier base importation exclusion-by-failure nonterminator defeasement
Surely there must be some *simpler things* that all this weird stuff is built out of?
And then the weird stuff can be a program?
Like, how do logicians argue about points of logic? They use some kind of logic to do it, right?
Shouldn't we just take whatever system logicians use, and code *that* up first?
Or are they actual wizards, and they settle arguments in the Journal of Constructivist Philosophical Logic by channelling their astral ether and turning other wizards into pies?
That might be difficult to code as a kernel proof algorithm, sure.
अायुष झा :question: @natecull I am not a logician, but I am a CS student and I have been studying logic for a few years now. They use mathematical constructs such as propositions and predicates, theorems and other verified proof
@ayys So, Prolog.
And yet, here's Rulelog, which 'combines much of the latest work in logic programming', but doesn't do it as, eg, propositions and predicates and theorems, but as a bunch of weird high-level stuff baked into the literal *syntax*.
This seems like putting several carts before a very tiny horse.
@natecull I hadn't heard about prolog before, but according to wikipedia, "Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of relations, represented as facts and rules" This doesn't sound too high level for me. Perhaps the prolog syntax is confusing?
@ayys .... you're in CS, and you've studied logic for years, but you've never yet heard of Prolog.....? O_O
I weep for CS. But I'm also kinda not surprised. Nobody seems to learn about anything older than five years ago.
Prolog is a 1970s language, so it's got 1970s problems - maybe you've heard of modern spiritual successor, Kanren?
@natecull Oops! I meant to say that I haven't used prolog. I think different parts of the world have different "preferred languages". I am from Nepal, and over on this side of the world, lisp is quite popular(I believe lisp is from the 1950s). In any case, I think knowledge representation is quite a difficult problem for programming languages.
@ayys Cool, Lisp at least is a good enough base for implementing Prolog on.
But seriously, you can't get very far in looking at computational logic before you hit Prolog (eg, unification by Robinson Resolution). Even today, most type theories are implemented in it.
It is a very small and simple logical proof algorithm that isn't amazingly clever but is at least mostly easy to understand.
@natecull I see. I am reading up on prolog right now. Thanks for getting me started! cheers!!
brennen@natecull how else do you expect us to calibrate the turboencabulator?