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 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?