1
$\begingroup$

I am reading article https://arxiv.org/pdf/cs/0511055v1.pdf (about defeasible deontic logic) and it mentions on page 10 the operator T that constructs extension (set of immediate consequences) from the theory D (set of statements). Such extensions form s.c. Kleene sequence and the fixed point exists for the operator T - this fixed point is the complete set of consequences of the set D of statements.

Such construction is known for many logics and I guess that it is the basis of the logic programming using forward chaining approach. This approach is known in business software as well and is called business rules (e.g. JBoss Rules Drolls of IBM ILOG). Such construction has very wide practical applications, e.g. if norms are encoded as logical statements then the set of consequences consist of all the obligations and permissions. More practical applications can be found as well - e.g. application of complex discounting rules in retail trade.

My theory question is:

  • Do I understand correctly that generation of set of consequences is the essence of logic programming and such logic programming can be devised for almost any logic?

My systems questions are:

  • Are there general framework (system) which receives 1) syntax of logic; 2) operator T and which generates program that can find set of consequences for any set D? I.e. should I construct logical programming tool for my logic from scratch (only parser can be generated automatically) of can I use some framework?
  • How such logic programming framework is connected with proof assistant and theorem prover frameworks (like Isabells of Coq)? As far as I understand then there is no connection - theorem provers use backward reasoning approach and logic programming uses forward reasoning approach? However - maybe any connections exists and maybe proof assistant/theorem prover frameworks can still be used for logic programming?
$\endgroup$
5
$\begingroup$

You understand incorrectly. That is not how logic programming works.

The number of consequences typically grows exponentially, or is even infinite. For instance, some consequences of $\forall x \in \mathbb{N} \,.\, \phi(x)$ are $\phi(0)$, $\phi(1)$, $\phi(2)$, $\phi(3)$, $\phi(3 + 2)$, $\phi(x \cdot 2)$, and so on. Generating all consequences is infeasable and useless. It's a bit like trying to write good literature by generating all grammatically correct sentences.

The gist of logic programming is proof search. A logic program follows a particular strategy to look for the proof of a given query. So in this sense, it does things backwards.

$\endgroup$
  • $\begingroup$ But there is vast are of production rules (also known as business rules). Then the questions arise: 1) how to guarantee that production rules completes their execution in finite time; 2) how production rules are related to logic programming. I think that logic programming is just formalization of production rules. and production rules use forward chaining (specifically Rete algorithm). $\endgroup$ – TomR Sep 25 '16 at 20:19
  • $\begingroup$ Sorry, I know nothing about business rules. But I know a bit about logic, and I explained to you that this is not how logic programming works. Someone else has to comment on these "business rules". Is there a reference that I can look at? $\endgroup$ – Andrej Bauer Sep 25 '16 at 20:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.