jeudi 23 février 2012

Less computers! More blackboards!

I'm currently doing an internship in a computer science research institute.

Actually we don't have blackboards, but white. And I still don't have my office, anyway.

During the next 5 months, I'm going to try to formalize the transformation of information in proof theory, with category theory as an approach of graph transformation.
Ok, that pretty much the title... I gonna try to explain that.

Concretely, a proof is a tree.
At the top, the leaves are the hypotheses, your materials to prove something.
Could be statements, or theorem already proved as inference rules.
And at the bottom, the root is what you want to prove, as a goal. A new brand theorem.
You combine hypotheses. Get new ones, given by application of intermediate theorems.
Until your goal pops out of all of these actions.

Every manipulations of your hypotheses, to reach your goal, is a transformation of the tree.
Mostly relations between hypotheses and theorems applied, to get sub goals.
A mini proof tree in the proof tree.

There is a field of computer science which formalizes transformation of information. With category theory on graph theory.
But it's another story, another day.

By now, I'm only reading past publications of my supervisors, or their phd students.
In march I'll start to take some exemples of proofs, simple ones, and formalize the transformations made to get the proof.
It's just pure gold...

9 commentaires:

MynameisEarl a dit…

Lol, that's a lot of hard words to understand there man. But I'm pretty sure that I get the gist of it.

So what you're saying is that (hypothetically) your proof (the tree) has a bunch of hypotheses (the leaves) that you have laid out. But in order to cement (root) your so called "proof" you must prove your hypotheses first. Only in doing so will cement your proof (root it down) and making it unable to be taken off by others willing to refute your claims.

I'm pretty that what I said made sense (it did for me), but all that computer lingo got me there mate. All I can say is good luck with your internship! :)

R Thornton a dit…

You pretty much lost me, but luckily I understand what you are talking about from my education.
-Ryan (

Simpetus a dit…

It makes sense... but it's not that.
you don't need to prove your hypotheses, you lay on them.

I didn't want to really extend on that, but ok :D
It's far more simple with examples and drawing.

We assume that we know only that.
.hypothesis 1°: 0=0
.hypothesis 2°: if x=x then x+1=x+1
_This one is pretty much a function.
_You give it x=x and it gives you x+1=x+1.

And want to know if that is true:
.goal: 2=2

My proof:

. .1°. . 2°
. . \___/ I use the hypotheses to prove a sub goal: 1=1
2°. .1=1
. 2=2 I reuse hypothesis and my fresh new sub proof to prove my goal.

And it looks like a tree.
Now, you actually start with a bunch of hypotheses
and organize them like a tree, step by step, tree by tree.
How you can "draw" your tree, step by step, is what I have to search.

More to come another time :)

DoceanMotion a dit…

I like that way you explained it! Good luck in your endeavors. :)

My 2 Pesos a dit…


Andy a dit…

That sounds really awesome. I'm studying computer science right now and I actually had to take a proof based course last semester. This is a really interesting approach to representing the course of a proof. Keep it coming!

Mik a dit…

As a CompSci student, looks pretty cool!

Bill Pliskin a dit…

Good luck!

troy a dit…

You lost me in the details, but good luck with your research.