Project ideas for automated deduction/automated theorem proving?

Question

Dear Stack Overflow brethren,

I'm a second-semester junior who will embark upon my thesis soon, and I have an interest in automated deduction and automated theorem provers. As in, I'd like to advance the art in some way (I don't mean that pretentiously, but I do want to do something productive). I've Googled pretty far and wide and so far few promising ideas have emerged. There are a few student project idea pages, but most seem either horribly outdated or too advanced (I was originally going to attempt to synthesize postmodernist thought (hahaha) and abstract its logical content, build a complete and consistent model (if possible, of course), and attempt to automate it, grounding said model as possible in a nonstandard logic a la these. My advisor thought that gave postmodernist thought too much credit (a while ago I reimplemented the Postmodernism Generator in Haskell with Parsec, so that is in part where the idea came from); I am tempted to concur.)

So, yeah. Does anyone have ideas? I apologize if there is some obvious gap in my approach here/if I haven't appropriately done my homework (and if there is one, please tell me!), but in large part I don't even know where to start, and thank you for reading all that.

Answer 1

Some negative advice. I'd avoid focusing on either boolean or first-order logic. They are areas that have been studied heavily, enough so that the limits of what is possible are fairly well understood. (There are even competitions to make FOL theorem provers.)

You might be able to make more progress looking at formal language descriptions like ontologies. I believe (but might be corrected) that the boundary between what is tractable, especially with an AI-assisted reasoner, and what is describable in full OWL is still not fully explored. The other ontology-related thing you could look at is ways to support more automated creation of ontologies in particular domains, though that might be a bit too much work for a sub-PhD level thesis.

Answer 2

Admitting up front that I'm not particularly well-informed about the field, I've been curious about the utility (and existence) of--for lack of a better term--"unreliable" proof assistant software, particularly as applied to problems that are, in general, intractable or undecidable. Systems based on heuristics or statistical analysis, that make "guesses" and stumble around trying to make things work, or things along those lines. The idea, of course, would be to toss it problems that aren't amenable to more methodical techniques based on exhaustive searching or rigorous deduction, possibly in bits and pieces as a component of an interactive proof assistant.

On the other hand, I don't know to what extent ideas along those lines have been explored already, and I'm not sure it's even a viable technique in the first place (if anyone else does know more, I'd be interested to hear it).