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

Browse archivesActive forum topics 
Recent comments
5 hours 21 min ago
6 hours 54 min ago
9 hours 58 min ago
10 hours 11 min ago
10 hours 29 min ago
11 hours 14 min ago
13 hours 31 min ago
14 hours 20 min ago
1 day 1 hour ago
1 day 4 hours ago