Restricting backtracking in connection calculi
Jens Otten · AI Communications · 2010
Connection calculi benefit from a goal-oriented proof search, but are in general not proof confluent. A substantial amount of backtracking is required, which significantly affects the time complexity of the proof search. This paper presents a simple