Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification |
| |
Authors: | Andrei Voronkov |
| |
Affiliation: | (1) Computing Science Department, Uppsala University, Box 311, S 751 05 Uppsala, Sweden |
| |
Abstract: | We characterize provability in intuitionistic logic with equality in terms of a constraint calculus. This characterization uncovers close connections between provability in intuitionistic logic with equality and solutions to simultaneous rigid E-unification. We show that the problem of existence of a sequent proof with a given skeleton is polynomial-time equivalent to simultaneous rigid E-unifiability. This gives us a proof procedure for intuitionistic logic with equality modulo simultaneous rigid E-unification. We also show that simultaneous rigid E-unifiability is polynomial-time reducible to intuitionistic logic with equality. Thus, any proof procedure for intuitionistic logic with equality can be considered as a procedure for simultaneous rigid E-unifiability. In turn, any procedure for simultaneous rigid E-unifiability gives a procedure for establishing provability in intuitionistic logic with equality. |
| |
Keywords: | intuitionistic logic equality rigid E-unification |
本文献已被 SpringerLink 等数据库收录! |
|