Efficient Rule-Matching for Automated Coherent Logic

Coherent logic is a syntactically defined fragment of first-order logic. The paper describes an experiment with a prover for coherent logic. A prover here means software that takes as input a theory in coherent logic, and (if it halts) either outputs a proof of a contradiction in the theory, or a model of the theory. Existing provers for coherent logic typically spend much of their time in the process of matching inferred literals with the negative literals of the input clauses. We present an alternative to this matching process by applying a modified version of the Rete algorithm [6]. The Rete algorithm was developed in the 1970s for production systems in artificial intelligence. We exploit the similarities between coherent logic and production systems in order to make the Rete algorithm solve the matching problem. We also investigate the effect of working on several independent branches present in proof search in coherent logic but not in production systems. NIK: Norsk Informatikkonferanse. 2012 (25-36). http://www.nik.no