Abstract:
In dialogue semantics, the logical constants receive a certain game-theoretical interpretation. Dialogues are games between two players, the proponent and the opponent, who can alternatingly either attack assertions made by the other player or defend their own assertions. The logical validity of an assertion made by the proponent in the first move consists in the existence of a winning strategy for the proponent for this assertion.
Based on a modified standard dialogue semantics for intuitionistic logic, we develop a formal dialogue semantics for definitional reasoning. Definitional reasoning is an extension of logic programming, in which an underlying logic can by extended by definitions of a certain form. The presented dialogue semantics is a semantics for logical reasoning with respect to such definitions. We also develop a formal dialogue semantics for implications considered as rules. Different to standard dialogue semantics for intuitionistic logic, this new semantics needs an additional argumentation form corresponding to cut. An equivalence result is proved for the resulting formal dialogue semantics and the intuitionistic sequent calculus for implications as rules.