Papers on Prolog-like languages without closed world assumption (CWA)

Question

Prolog execution process may be seen as a search that model scientific search for a proof of a proposition. At the same time, real world scientific search greatly differs from Prolog search in the following way:

As we know, Prolog is based on closed world assumption (CWA) -- that is, if a proposition is not in the fact database and not derivable from the fact database, then it is not true. So Prolog search may yield 2 results:

• proposition is proved; here is the proof: ...
• proposition is false or it can not be proved using fact database

At the same time, scientific search is not limited by CWA and may be seen in at least 4 states:

• proposition is proved; here is the proof: ...
• proposition is disproved by counter-example; here is the counter-example: ...
• proposition is neither proved, nor disproved to the specified (current) time
• proposition is proved to be independent from the axiom set; here is the proof: ...

I suspect that, because of popularity of Prolog in the end of the XX century, there were successful attempts to improve it by removing CWA in order to better model scientific search in resulting language. CWA removing seems to open possibility to use 3 or even all the 4 above-mentioned states in programming language execution process.

So, I suspect, there are papers that describe such attempts and explore theoretic foundations of such a prolog-like languages. If so, please point out a survey or a bunch of most significant of such a papers.

Answer 1

Thank you for a great question! I am looking into papers on related subjects myself--I'll post anything worthwhile that I come across, and would appreciate if you would do the same. = ) Off the top of my head, you might be interested in ileanTAP, a Prolog theorem prover for intuitionistic logic (includes a short paper). Just so the term is not left undefined:

Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either. In constructive logic, a statement is 'only true' if there is a constructive proof that it is true, and 'only false' if there is a constructive proof that it is false. Operations in constructive logic preserve justification, rather than truth. (Wikipedia)

Have you read Kuhn on scientific paradigm shifts? The problem you have described is generally applicable to all of science: theories (and coherent theoretical domains) are abstracted axiomatic systems, and updating a scientific domain (as opposed to "filling out the missing bits" by using what's already established as "axioms") requires switching from one isomorphic system to another (two systems are isomorphic if they have identical or similar outputs for some narrow set of parameters, e.g. Newtonian physics and GR).