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

Browse archivesActive forum topics 
Recent comments
22 hours 19 min ago
23 hours 8 min ago
1 day 5 hours ago
1 day 7 hours ago
1 day 15 hours ago
1 day 15 hours ago
1 day 16 hours ago
1 day 17 hours ago
1 day 20 hours ago
1 day 23 hours ago