University of Cambridge > > Computer Laboratory NetOS Group Talklets > Culture clash: logic meets the real world

Culture clash: logic meets the real world

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Heidi Howard.

Research on the automation of reasoning has made huge advances during recent decades. There is an increasing number of logic tools, of ever increasing strength, and supporting an increasing number of applications.

But something is rotten in the state of logic tool implementations. It’s still highly nontrivial to move logical evidence (especially proofs) between tools. This restricts what we can do with these tools.

Now at this point you might be thinking, “why’s this relevant to NetOS?”. Well, everything’s connected, right? :) Despite occurring in logic tools, this problem’s essence isn’t a logic problem: it’s essentially to do with system integration.

The difficulty described above arises because logic tools are just tools: they suffer from the same shortcomings of other software. Particularly research tools. Their documentation is often stale, the tools’ behaviour is badly specified, and the information they emit is often not sufficiently detailed to reconstruct in other tools.

I’ll talk about an approach that makes the transfer of data across logic tools more robust in the presence of such setbacks. This relies on two ideas: compiler phases, and a more principled form of “tag soups”. Logic tools need systems thinking.

This talk is part of the Computer Laboratory NetOS Group Talklets series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2021, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity