User loginNavigation 
Cyclic Proofs for FirstOrder Logic with Inductive DefinitionsCyclic Proofs for FirstOrder Logic with Inductive Definitions, James Brotherston, in Proceedings of TABLEAUX 2005
This technique of making potentially cyclic proofgraphs is really nice since it makes the connection between recursive definitions in a functional programming language and a proof structure very obvious. There is no need to specify the inductive principle ahead of time, you can simply structure the proof tree as you would your functional code. By Gavin MendelGleason at 20080128 20:33  LtU Forum  previous forum topic  next forum topic  other blogs  3232 reads

Browse archivesActive forum topics 
Recent comments
1 week 5 days ago
1 week 6 days ago
1 week 6 days ago
3 weeks 2 days ago
3 weeks 2 days ago
3 weeks 3 days ago
3 weeks 3 days ago
3 weeks 3 days ago
3 weeks 3 days ago
3 weeks 3 days ago