Teaching Prolog by providing counter examples: A model generator for Datalog plus Cut

Help!
1

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,
Stefan

2

I did not try to work through your examples but as I read this two thoughts came to mind.

  1. Halting problem - Be warned that AFAIK the halting problem is typically applied to Turning complete languages but for systems that are not Turning complete some can be proved to halt, e.g. Mathematical calculus..
    Here is an article that can give some futher background but I have not checked it, nor do I have the all the skills to check it. Solving the halting problem
  2. Fuzzing - See Logtalk QuickCheck and pay attention to shrinking. Note: SWI-Prolog has Auto-generating tests but AFAIK it is not as mature as what is done in Logtalk.
3

Its a wild idea, but you could have a look at the new monotonic tabling support. If you define the facts as dynamic monotonic and all predicates as tabled monotonic and you run the thing you end up with a graph (the IDG, Incremental Dependency Graph) of continuations that link the facts and tables. I don’t know really how the story goes on (and it isn’t really clear to me what you want), but who knows what it triggers :slight_smile:

I guess you want to define a domain for the variables? Without I doubt this can be answered. Simply running the toplevel with some arbitrary binding and see which database queries are asked may be a step. Here too, incremental tabling may help to find the dependencies and reason about repair strategies.

1 Like
4

Thank you for the quick response. I am not yet familiar with the monotonic tabling support, but will have a look at it.

What I want, i.e. my application in mind, is to teach Prolog programming by providing counter examples. The first exercise in my class is typically something like the following:

Assume you have a database relation db1(Members,NumberOfCitations).
Write a program that finds all the Members M in db1 having a maximum 
NumberOfCitations N  - with using only Datalog + comparisons + negation, 
i.e., without using built-in predicates like findall, min, ... .

A possible correct solution would be

   correct_solution(M) :- db1( M , N ) , \+ greater_N2_found_than( N ) . 
   greater_N2_found_than( N ) :- db1( _ , N2 ) , N2 > N .

A typical error which I have seen hundreds of times in the students’ programs is

   student_solution(M) :- db1( M , N ) , db1( _ , N2 ) , N > N2 .

i.e. the student’s program returns members having more citations than another member, but not those members having a maximum number of citations.
In such a case, I do not want to show the correct solution, but I want to create a counter example database state S that demonstrates why their solution is wrong, such that they can try to improve their solution.

An example of such a counter example database state S is

db1(1,100). 
db1(2,200).
db1(3,300).

My test program evaluates both programs on this counter example database state S and returns:

The student_solution is not equivalent to correct_solution. 
For example, for the database state S given above, 
the correct solution returns 
          3
however, the student_solution returns, 
          2
          3
          3

Currently, I generate the counter example database state S by hand (based on the knowledge of typical programming errors). What I want instead is to generate the counter example database state S automatically from the correct_solution and from the student_solution.

The idea is the following. I want to search a counter example database state S, for which the following procedure

   counter_example(M) :- correct_solution(M) , \+ student_solution(M) . 
   counter_example(M) :- student_solution(M) , \+ correct_solution(M) .

returns anything different from false. Because, if

   ?-counter_example(M).

is satisfiable, then there is a difference in both solutions; and I can use this counter example database state S to demonstrate why the student_solution is wrong.
That is why I saerch a model (=a database state S) that makes the query

   ?-counter_example(M).

satisfiable.

For my application, it would be absolutely o.K. to restrict the domain of all the variables to a subset of integer, e.g. to assume, all values are in 0…1000 .
Furthermore, it would be o.K. to limit the number of database relations to e.g. 4 and to limit the maximum number of parameters per database relation to 4 (we do not have more in our practical exercises).

Any comments are appreciated,

Stefan

5

Hi, Stefan. I recognise the problem you describe as a problem of abductive learning. Briefly, (logical) abduction is a third type of logical inference, along with induction and deduction. My crude explanation using a mix of Prolog and more general logic programming terminology is that deduction is the derivation of new atomic formulae (atoms, not in the Prolog sense) from rules and facts, induction is the derivation of new rules and abduction is again the derivation of new atoms. The difference between abduction and deduction is that deduction derives positive atoms, or the head literals of clauses, whereas abduction derives negative atoms, so the body literals of clauses. Seen another way, deduction derives the conclusions while adbuction derives the premises of implications (represented as clauses).

There’s a large body of liteature on abductive reasoning and abductive learning (part of the broader field of Inductive Logic Progamming) and I think what you want to do is possible in one of the abductive learning frameworks. Unfortunately I’m not terribly familiar with abductive learning but as far as I know the foundational text is Abductive Concept Learning by Kakas and Riguzzi, published in 2000:

Alternatively, you could try to re-formulate the problem as an inductive learning problem. For instance, you could give examples of the predicate db1/1 and learn a definition (a set of definite clauses) using an inductive learning system such as Aleph, Progol, Metagol, etc. I’m happy to help if you can accept this kind of conversion.