Conversation

Talia Ringer 🌻🪬
@TaliaRinger
Honestly after reading the history of the Stanford AI Lab, I'm now even more confused about what the difference between PL and symbolic AI is. Like Lisp was an AI thing? Really? Did we just rename huge swaths of Symbolic AI to PL to avoid the stigma of the AI winter?
20
108
Liam O'Connor
@kamatsu8
For one thing, Isabelle's emphasis on automation and Coq's emphasis on inductive structures reflects the research interests of the people who made it.
2
5
Talia Ringer 🌻🪬
@TaliaRinger
Yeah true. TBH I think automation is often much easier in constructive logics, and the fact that classical proof assistants are more automated is an artifact of history
2
1
Liam O'Connor
@kamatsu8
I don't know why you say that, but I'd be willing to be convinced. The main source of great automation in Isabelle is the ability to rewrite by thousands of equalities, and therefore the very flexible notion of equality in Isabelle that supports e.g. quotients
3
4
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more