references to the regular world assumption and schemas

momigliano

Carsten Schuermann "Automating the Meta Theory of Deductive Systems "
Brigitte Pientka "Programming with proofs and explicit contexts," PPDP 08

gares

thanks!

momigliano

on second thoughts, adiscussion about the RWA is easier to spot in
"Benchmarks for Reasoning with with Syntax Trees Containing Binders and Contexts of Assumptions." http://momigliano.di.unimi.it/papers/mscs.pdf and there's is an Abella plugin described in
Olivier Savary Bélanger, Kaustuv Chaudhuri:
Automatically Deriving Schematic Theorems for Dynamic Contexts, LFMTP14

gares

I'll check this other paper. I've started reading the PhD manuscript of Carsten, around page 100 I found this (SOME...BLOCK...) syntax. It indeed seems that in our proofs/criteria it may make sense to reason about a context block as a whole. Thanks again for the pointers.