24 citations · 43 across the 16 of their papers we have counts for
6 papers · 1 filter
Isabelle Formalisation of Original Representation Theorems
Marco B. Caminati
In a recent paper, new theorems linking apparently unrelated mathematical objects (event structures from concurrency theory and full graphs arising in computational biology) were d…
Representation Theorems Obtained by Miningacross Web Sources for Hints
Marco B. Caminati, Juliana K. F. Bowles
A representation theorem relates different mathematical structures by providing an isomorphism between them: that is, a one-to-one correspondence preserving their original properti…
Correct Composition of Dephased Behavioural Models
Juliana Bowles, Marco B. Caminati
Scenarios of execution are commonly used to specify partial behaviour and interactions between different objects and components in a system. To avoid overall inconsistency in speci…
A Verified Algorithm Enumerating Event Structures
Juliana Bowles, Marco B. Caminati
An event structure is a mathematical abstraction modeling concepts as causality, conflict and concurrency between events. While many other mathematical structures, including groups…
Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?
Marco B. Caminati, Manfred Kerber, Christoph Lange +1
When faced with the question of how to represent properties in a formal proof system any user has to make design decisions. We have proved three of the theorems from Maskin's 2004…
A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
Christoph Lange, Marco B. Caminati, Manfred Kerber +4
Novel auction schemes are constantly being designed. Their design has significant consequences for the allocation of goods and the revenues generated. But how to tell whether a new…