Finding Unity in Computational Logic

Dale Miller (1, 2)

1 PARSIFAL - Proof search and reasoning with logic specifications
2 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]

While logic was once developed to serve philosophers and mathematicians, it is increasingly serving the varied needs of computer scientists. In fact, recent decades have witnessed the creation of the new discipline of Computational Logic. While Computation Logic can claim involvement in diverse areas of computing, little has been done to systematize the foundations of this new discipline. Here, we envision a unity for Computational Logic organized around the proof theory of the sequent calculus: recent results in the area of focused proof systems will play a central role in developing this unity.

Domaines: Logique en informatique [cs.LO]

Dale Miller. Finding Unity in Computational Logic. ACM-BCS Visions of Computer Science, 2010, Edinburgh, United Kingdom. ⟨hal-00772557⟩