Matthew Wampler-Doty

less info
352 reputation
28
bio website w-d.org
location South Park, Colorado
age 29
visits member for 3 years, 9 months
seen Apr 9 at 16:11
I am working on my MSc in Logic at the ILLC at Universiteit van Amsterdam. I am interested in automated deduction, formal logic, proof theory, computation, abstract algebra, game theory, and category theory.

Jun
25
awarded  Yearling
Jun
25
awarded  Citizen Patrol
Jul
9
revised Bicartesian closed categories and Heyting algebras
added 232 characters in body
Jul
9
awarded  Scholar
Jul
9
accepted Bicartesian closed categories and Heyting algebras
Jul
8
revised Bicartesian closed categories and Heyting algebras
Add equational axiomatization regarding Heyting algebras
Jul
8
answered Non-constructive proofs of decidability?
Jul
8
asked Bicartesian closed categories and Heyting algebras
Jul
8
awarded  Critic
Jul
8
awarded  Nice Answer
Jul
8
revised How do they verify a verifier of formalized proofs?
added 171 characters in body; edited body
Jul
7
revised How do they verify a verifier of formalized proofs?
added 156 characters in body
Jul
7
comment Are there any good nonconstructive “existential metatheorems”?
One example of this is where Y is "first order tableaux proof systems" and "X" is the cut rule. In his paper "Don't Eliminate Cut", George Boolos gives a problem which a tableaux with the cut rule can prove in about a page of symbols, but without cut it takes more symbols than there are atoms in the universe. @Darsh - "Don't Eliminate Cut" shows the difficulty can indeed be "can't be done effectively in general" in some situations. Here's Boolos' paper: springerlink.com/content/pj2775t3j0435262
Jul
7
awarded  Necromancer
Jul
7
answered How do they verify a verifier of formalized proofs?
Jul
7
answered Is there any proof assistant based on first-order logic?
Jul
6
awarded  Supporter
Jul
6
awarded  Autobiographer
Jul
5
revised Are there any good nonconstructive “existential metatheorems”?
added 83 characters in body
Jul
5
awarded  Editor