何かの定理を証明するときに、何をしてよいのか困ったことはありませんか？数学の定理の証明は「公理」から「推論」を組み合わせて導きます。

公理とは証明抜きに真とされる仮定で、例えば群の公理は群が満たすべき条件をあげて、どういうものが群であるか規定します。
「推論」とは何から何を帰結してよいのか規定する規則です。例えば「『AならばB』で、さらに『A』であるとき『B』と帰結してよい」三段論法は推論規則の一つです。

　私の研究はざっくりいうと「どんな公理とどんな推論規則を許したときに、何が帰結できるのか」を明らかにすることを目的としています。
普段はあまり意識することはないと思いますが、通常の数学の大半の定理ははZFC集合論と呼ばれる集合論の公理から古典論理と呼ばれる推論規則を使って証明されます。

　しかしこれが唯一の正しい公理と論理ではありません。例えば、真なる命題とは証明が与えられたものである、というモチベーションをもとに推論規則を組み立てると、未解決問題に対しては「AまたはAでない」が成り立つとは言えません。
計算機で証明が書けるものを真と考えても同様のことが言え、このことは実際に自動証明や定理証明支援系の理論的なバックグラウンドになります。このように通常と違う推論を用いて数学をやってみると、普通の数学と大分違った世界が見えてきて、とても楽しいです。