Have you ever been unsure about what to do when trying to prove a theorem? The proof of mathematical theorems is derived by combining "axioms" and "inferences".

Axioms are assumptions which are assumed to be true whithout proof. For example, the axiom of groups specifies the conditions that a group must satisfy and defines what a group is.
"Inferences" are rules that determine what conclusions can be drived from what assumptions. For example, the modus ponens "if A then B", and "A", therefore "B" is one inference rules.

My research aims, in a word, to reveal "what can be concluded when given any axioms and inference rules".
Although we usually don't pay much attention to it, most of the theorems in ordinary mathematics are formalized and proved using the axioms of set theory called ZFC and the inference rules of classical logic.

However, this is not the only correct set of axioms and logic. For example, if we build inference rules based on the motivation that a proposition is true if a proof is given, we cannot necessarily conclude "A or not A" for unresolved problems.
Even considering proofs written by computers as true leads to the same issue, which becomes a theoretical background for automated theorem proving and proof assistance systems.
When we try to do mathematics using different inferences than usual, we can see a world that is quite different from ordinary mathematics, which is very exciting.