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  3131 reads

Browse archivesActive forum topics 
Recent comments
6 hours 6 min ago
1 day 6 hours ago
1 day 7 hours ago
1 day 8 hours ago
2 days 13 hours ago
2 days 14 hours ago
3 days 9 hours ago
3 days 10 hours ago
3 days 10 hours ago
4 days 2 hours ago