What are constraints on some new logic programming language and system?

Question

As I understand, everyone can create logic programming language and system by declaring that the valid program of some logic programming language is the set of statements in the form: body->head, where body is arbitrary expression of boolean type and the head is set of expression that, in some cases, can change the current valuation function (function for some logic that assigns values to the variables of this logic), e.g. by assignment operations. There is no need to prove any properties of such programming system, because one can expect that such system is Turing complete and hence there is no important properties (e.g. termination) to prove. Practical termination can be achieved even by very rude methods (e.g. as in Drools), e.g. by allowing to declare that no more than e.g. 10 rules can be fired in one execution step. Am I right? Does the definition of new logic programming system/language for scientific and practical purposes ineed allow such great freedom without any constraints and duties to prove some properties of this system?

Of course, some works on logic programming tries to prove stable model properties but I am interested (and practice usually requires) in non-monotonic logic programs (as almost any program used for business purposes change the state and hence the valuation function of variables) and they can not have such stable models.

There is such background for my question: I am aware of the logic programming system for agent modelling http://jason.sourceforge.net/wp/ Jason AgentSpeak. I am not satisfied with the expressibility of the base logic used by AgentSpeak. I have reason to state, that special kind of linear logics can be more appropriate base logic for agent modelling. That is why I am trying to create my own new logic programming system that is based on special kind of modal linear logic with actions. So - can I simply form the set of expressions of the type body->head from the language of modal linear logic and announce them as logic programs in modal linear logic? I am required to prove anything?

Answer 1

It sounds like you have the impression that there are some rules on what languages you are allowed to define. There are no such rules. You can define whatever language you want. You can do whatever what you want -- you're not required to do anything (there are no language police who will come arrest you for failing to prove some theorem about it). Whether it will be useful, or used by anyone else, is a different matter.

Answer 2

An interpreter for a logic programming language is usually based on a proof systems that has been proven sound and complete, like definite clause resolution that Prolog uses. Of course you could implement that in any way you like, but if that implementation itself uses some declarative form of programming, it may be easier to argue that your implementation is correct in regards to the proof system, although generally this is left for experience (if there are many users, they will detect cases where the interpreter isn't working as it should). Regarding Jason, the belief base of an agent can be customised, so if you want to use AgentSpeak and the agent infrastructure for your system's practical reasoning and just use a different logic for the beliefs, that's possible. But that doesn't seem to be the case, you'd like to reason about action differently so Jason won't help in your case, although it may be useful to use part of it's code if you want to implement your interpreter in Java, or you could implement your interpreter on top of AgentSpeak if that helps for your particular interpreter.