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

Browse archives
Active forum topics 
Recent comments
7 weeks 3 days ago
7 weeks 3 days ago
7 weeks 3 days ago
29 weeks 4 days ago
33 weeks 6 days ago
35 weeks 4 days ago
35 weeks 4 days ago
38 weeks 1 day ago
42 weeks 6 days ago
42 weeks 6 days ago