Abstract

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.