A Complete Subsumption Algorithm

Abstract. Efficiency of the first-order logic proof procedure is a major issue when deduction systems are to be used in real environments, both on their own and as a component of larger systems (e.g., learning systems). Hence, the need of techniques that can perform such a process with reduced time/space requirements (specifically when performing resolution). This paper proposes a new algorithm that is able to return the whole set of solutions to θ-subsumption problems by compactly representing substitutions. It could be exploited when techniques available in the literature are not suitable. Experimental results on its performance are encouraging.

• Type: Conference
• Year: 2003
• Where: AIIA
• Authors: Stefano Ferilli, Nicola Di Mauro, Teresa Maria Altomare Basile, Floriana Esposito
• Keywords: AIIA 2003, Artificial Intelligence, Deduction Systems, Logic Proof Procedure, Time/space Requirements