Problem solving by searching for models with a theorem prover

摘要

Given a problem described as a set of rules or constraints, finding solutions that satisfy these constraints is a central task in the area of artificial intelligence. We present a theorem prover that can solve a problem by searching for models. The problem representation it accepts is in first-order logic which is fully declarative. The solutions obtained are logical consequences of the constraints, so they are correct. Negative information can be asserted and processed correctly. Finally, if the problem has multiple solutions, all of them can be found.