Basic first-order model theory in Mizar. - Marco B. Caminati (J. Formaliz. Reason., 2010)

Preliminaries to Classical First Order Model Theory. - Marco B. Caminati (Formaliz. Math., 2011)

Definition of First Order Language with Arbitrary Alphabet. Syntax of Terms, Atomic Formulas and their Subterms. - Marco B. Caminati (Formaliz. Math., 2011)

First Order Languages: Further Syntax and Semantics. - Marco B. Caminati (Formaliz. Math., 2011)

Free Interpretation, Quotient Interpretation and Substitution of a Letter with a Term for First Order Languages. - Marco B. Caminati (Formaliz. Math., 2011)

Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem. - Marco B. Caminati (Formaliz. Math., 2011)

A simplified framework for first-order languages and its formalization in Mizar - Marco B. Caminati (CoRR, 2012)

A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. - Christoph Lange 002; Marco B. Caminati; Manfred Kerber; Till Mossakowski; Colin Rowat; Makarius Wenzel; Wolfgang Windsteiger (MKM/Calculemus/DML, 2013)

Proving soundness of combinatorial Vickrey auctions and generating verified executable code. - Marco B. Caminati; Manfred Kerber; Christoph Lange 002; Colin Rowat (CoRR, 2013)

Custom Automations in Mizar. - Marco B. Caminati; Giuseppe Rosolini (J. Autom. Reason., 2013)

Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle? - Marco B. Caminati; Manfred Kerber; Christoph Lange 002; Colin Rowat (CICM, 2014)

Budget Imbalance Criteria for Auctions: A Formalized Theorem. - Marco B. Caminati; Manfred Kerber; Colin Rowat (CoRR, 2014)

Pseudo-Canonical Formulae are Classical. - Marco B. Caminati; Artur Kornilowicz (Formaliz. Math., 2014)

Sound Auction Specification and Implementation. - Marco B. Caminati; Manfred Kerber; Christoph Lange 002; Colin Rowat (EC, 2015)

VCG - Combinatorial Vickrey-Clarke-Groves Auctions. - Marco B. Caminati; Manfred Kerber; Christoph Lange 002; Colin Rowat (Arch. Formal Proofs, 2015)

Mind the Gap: Addressing Behavioural Inconsistencies with Formal Methods. - Juliana Küster Filipe Bowles; Marco B. Caminati (APSEC, 2016)

Correct Composition of Dephased Behavioural Models. - Juliana Bowles; Marco B. Caminati (FACS, 2017)

A Flexible Approach for Finding Optimal Paths with Minimal Conflicts. - Juliana Küster Filipe Bowles; Marco B. Caminati (ICFEM, 2017)

A Verified Algorithm Enumerating Event Structures. - Juliana Bowles; Marco B. Caminati (CICM, 2017)

An integrated framework for verifying multiple care pathways. - Juliana Bowles; Marco B. Caminati; Suhyun Cha (TASE, 2017)

An Integrated Approach to a Combinatorial Optimisation Problem. - Juliana Bowles; Marco B. Caminati (IFM, 2019)

A framework for automated conflict detection and resolution in medical guidelines. - Juliana Bowles; Marco B. Caminati; Suhyun Cha; Juan Mendoza (Sci. Comput. Program., 2019)

Balancing Prescriptions with Constraint Solvers. - Juliana Küster Filipe Bowles; Marco B. Caminati (Automated Reasoning for Systems Biology and Medicine, 2019)

A Formally Verified SMT Approach to True Concurrency. - Juliana Küster Filipe Bowles; Marco B. Caminati (CILC, 2020)

Correct composition in the presence of behavioural conflicts and dephasing. - Juliana Küster Filipe Bowles; Marco B. Caminati (Sci. Comput. Program., 2020)

Representation Theorems Obtained by Mining across Web Sources for Hints. - Marco B. Caminati; Juliana Küster Filipe Bowles (ICICT, 2023)

Isabelle Formalisation of Original Representation Theorems. - Marco B. Caminati (CICM, 2023)

Representation Theorems Obtained by Miningacross Web Sources for Hints. - Marco B. Caminati; Juliana Küster Filipe Bowles (CoRR, 2023)

O2 is a Multiple Context-Free Grammar: An Implementation-, Formalisation-Friendly Proof. - Marco B. Caminati (DLT, 2024)