329 citations · 459 across the 19 of their papers we have counts for
21 papers
DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments
Aaron Bryce, Rajeev Gore'
Gentzen's 1936 proof of the consistency of Peano Arithmetic was a significant result in the foundations of mathematics. We provide here a modified version of the proof, based on Gö…
A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
Ian Shillito, Iris van der Giessen, Rajeev Goré +1
We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic , an intuit…
N-PAT: A Nested Model-Checker
Hadrien Bride, Cheng-Hao Cai, Jin Song Dong +4
N-PAT is a new model-checking tool that supports the verification of nested-models, i.e. models whose behaviour depends on the results of verification tasks. In this paper, we desc…
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
Tim Lyon, Alwen Tiu, Rajeev Goré +1
We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this met…
Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)
Rajeev Goré, Björn Lellmann
We give a linear nested sequent calculus for the basic normal tense logic Kt. We show that the calculus enables backwards proof-search, counter-model construction and syntactic cut…
A case study in formal verification of a Java program
Dmitry Brizhinev, Rajeev Goré
We describe a successful attempt to formally verify a simple genetic algorithm written in Java. To this end, we compare several formal verification tools designed for Java, and sel…