13 citations · 26 across the 18 of their papers we have counts for
18 papers
On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone Theorem
Rob Arthan, Paulo Oliva
In this paper we present a quantitative analysis of the first and second Borel-Cantelli Lemmas and of two of their generalisations: the Erdős-Rényi Theorem, and the Kochen-Stone Th…
Negative Translations for Affine and Lukasiewicz Logic
Rob Arthan, Paulo Oliva
We investigate four well-known negative translations of classical logic into intuitionistic logic within a substructural setting. We find that in affine logic the translation schem…
Studying Algebraic Structures using Prover9 and Mace4
Rob Arthan, Paulo Oliva
In this chapter we present a case study, drawn from our research work, on the application of a fully automated theorem prover together with an automatic counter-example generator i…
A Curry-Howard Correspondence for the Minimal Fragment of Łukasiewicz Logic
Rob Arthan, Paulo Oliva
In this paper we introduce a term calculus which adds to the affine -calculus with pairing a new construct allowing for a restricted form of contraction. We obtain a…
On the Jaśkowski Models for Intuitionistic Propositional Logic
R. D. Arthan
In 1936, Stanislaw Jaśkowski gave a construction of an interesting sequence of what he called "matrices", which we would today call "finite Heyting Algebras". He then gave a very b…
Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
Yuhui Lin, Gudmund Grov, Rob Arthan
The use of a functional language to implement proof strategies as proof tactics in interactive theorem provers, often provides short, concise and elegant implementations. Whilst be…