I am working on a teaching application that shall help students to learn Prolog by providing counter examples for wrong code.
Therefore, currently, I consider incomplete programs written in a subset of Prolog,
i.e. Datalog + comparisons (e.g. X>Y) + Negation_as Failure + Cut .
The programs are incomplete in the sense that for some of the predicates, so called database predicates, no facts or rules are given.
I am searching for an algorithm (or a hint/link that this an unsolvable problem) which can do the following:
For an arbitrary query, the algorithm should generate a model that makes the query satisfiable. In other words, the algorithm should find facts for the database predicates, such that the query is satisfiable.
For example, the query might be ?- counter_example(M) .
And the incomplete program might be:
counter_example(M) :- correct_solution(M) , \+ student_solution(M) . counter_example(M) :- student_solution(M) , \+ correct_solution(M) . correct_solution(M) :- db1( M , N ) , \+ greater_N2_found_than( N ) . greater_N2_found_than( N ) :- db1( _ , N2 ) , N2 > N . student_solution(M) :- db1( M , N ) , db1( _ , N2 ) , N > N2 .
In this case, the desired output could be e.g.
db1( 1, 100 ) .
db1( 2, 200 ) .
db1( 3, 300 ) .
as this database state makes the query ?-counter_example(M). satisfiable.
In general, there might occur more than just one database relation (here only db1) in the program, and then, I want to get a database state that contains multiple database relations, such that the counter_example query is satisfiable. Database relations may also be empty (i.e. contain no fact).
It would be great to solve the problem (to have an algorithm) also for checking satisfiability of programs that may contain a Cut.
I would appreciate any hints or comments,