fmidue / logic-tasks

0 stars 1 forks source link

Resolution von Klauseln in "Prolog Notation" sollte nur Hornklauseln enthalten #72

Closed nimec01 closed 9 months ago

nimec01 commented 10 months ago

Behebt #54. genPrologInst generiert nun nur PrologInst mit Hornklauseln. Ich habe dementsprechend auch ein Testcase erstellt, welches erfolgreich durchlaufen wird.

jvoigtlaender commented 10 months ago

Two further aspects:

  1. The constraint here should probably be controled by a config option. Just in case someone wants to use the task type also for more general situations. But something like createOnlyHornClauses = True could be the default. Or even a more specific name, depending on the 2. point.
  2. The original motivation was to have only clauses that can appear in the context of Prolog resolution. But then the constraint could be even more specific. Instead of "two horn clauses" it would be "two horn clauses, one of which consists only of negative literals". What do you think @owestphal, should it be refined thus?
owestphal commented 9 months ago

I think the principled approach would be to change the underlying genClause-Generator to take an additional argument of some type like

data ClauseShape = AnyClause | HornClause HornShape
data HornShape = AnyHornClause | Fact | Procedure | Query

and generate the respective type of clause.

Then, the configuration of (Prolog) resolution tasks could have configuration options like firstClauseShape :: ClauseShape, secondClauseShape :: ClauseShape, ...

jvoigtlaender commented 9 months ago

I like the idea of using the ClauseShape and HornShape types and replacing createOnlyHornClauses in PrologConfig by firstClauseShape :: ClauseShape and secondClauseShape :: ClauseShape.

But let's not go for parametrizing genClause right now. Instead, refashion isHornClause :: PrologClause -> Bool into a function hasTheClauseShape :: ClauseShape -> PrologClause -> Bool and replace https://github.com/fmidue/logic-tasks/blob/4e0df5d3a6230100670f4e14b6c44ba5edd66c91/src/LogicTasks/Semantics/Prolog.hs#L37 by:

  `suchThat` \(PrologInst clause1 clause2 _) -> hasTheClauseShape firstClauseShape clause1 && hasTheClauseShape secondClauseShape clause2

If at any point we do feel like actually changing genClause to take a ClauseShape argument, we can then move hasTheClauseShape over to the test suite, testing genClause.

nimec01 commented 9 months ago

I have added a few checks so that you cannot create a PrologConfig with which no resolution is possible.