formulas(assumptions). % First-order logic and DLs are based on the open world assumption. % If we want to say that a relation is true only for some specific values, we have to specify closure axioms! % To forget these axioms is a common mistake... cell(11). cell(12). cell(13). cell(21). cell(22). cell(23). cell(31). cell(32). cell(33). % closure axiom for cell all x (cell(x) -> x = 11 | x = 12 | x = 13 | x = 21 | x = 22 | x = 23 | x = 31 | x = 32 | x = 33). adj(22,11). adj(22,12). adj(22,13). adj(22,21). adj(22,23). adj(22,31). adj(22,32). adj(22,33). % closure axiom for adj all x all y (adj(x,y) -> cell(x) & cell(y)). contains(22,1). -mine(11). -mine(12). -mine(13). -mine(21). -mine(22). -mine(23). -mine(31). -mine(32). % these three axioms are equivalent all x (contains(x,1) -> exists z (adj(x,z) & mine(z) & all y (adj(x,y) & mine(y) -> y = z))). %all x (contains(x,1) -> exists z (adj(x,z) & mine(z) & all y (y != z & adj(x,y) -> -mine(y)))). %all x (contains(x,1) -> exists z (adj(x,z) & mine(z) & -(exists y (y != z & adj(x,y) & mine(y))))). end_of_list. formulas(goals). mine(33). end_of_list.