Extending Semantic Resolution via Automated Model Building: Applications

Abstract

An extension of sema ntic reso luti on is proposed. It is also an extension of th e set of s upp o rt as it ca n be considered as a particular ca se of se mantic reso luti on. It is proved sound and refu tat ionally co mpl ete. Th e extension is based on o ur form er m et hod for mod el building. The ap pr oach us es co nstrain ed cl aus es (or c-clauses), i. e. co uples [claus e : co n s traint]. Two imp o rt ant new fe atures are introduced with r es pect to sem antic resolution . Firstly, the m et hod builds its o wn (finite or infinite) models to guide the search or to stop it if th e initial set of clauses is satisfiable. S ec ondly, inst ea d of evalu at ing a clause in an int e rpr etat ion it imposes conditions (coded in its rules) to force a c-clause n ot to be evaluated to true in th e interpre tati on it builds . Th e extension is limit ed in this pap er to binary resolution but generalizing it to nary-resolution should be st ra ightforward . The prover impl em ent ing our method is an extension of OTTER and co mp ares advantageously with it (if binary reso luti on is used in OTTER) , both in the search space and in th e pr oof le nght of a releva nt non t rivi al exa mpl e. L ast but not least, mod el building is in crem ental. This featu re is specially useful when dealing with large set of claus es .