<p>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 <a href="http://www.leancop.de/ileantap/" rel="nofollow">ileanTAP, a Prolog theorem prover for intuitionistic logic</a> (includes a short paper). Just so the term is not left undefined:</p>

<blockquote>
  <p>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)</p>
</blockquote>

<p>Have you read <a href="http://en.wikipedia.org/wiki/Paradigm_shift#Kuhnian_paradigm_shifts" rel="nofollow">Kuhn on scientific paradigm shifts</a>? 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).</p>

CC BY-SA 3.0
2012-11-13T17:24:17.913Z
[Computer derives natural laws from raw data](http://www.news.cornell.edu/stories/April09/NaturalLaws.ws.html)--while this project took the essentially opposite, bottom-up from scratch approach: "The researchers found that seeding the complex pendulum problem with terms from equations for the simple pendulum cut processing time to seven or eight hours. This "bootstrapping," they said, is similar to the way human scientists build on previous work." It seems that giving their computer a Prolog-like repository would speed up its heuristics.
QuietThud
CC BY-SA 3.0
2012-11-13T07:52:37.543Z
2012-11-13T08:21:52.790Z
2012-11-13T08:21:52.790Z
QuietThud
<p>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:</p>

<p>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:</p>

<ul>
<li>proposition is proved; here is the proof: ...</li>
<li>proposition is false or it can not be proved using fact database</li>
</ul>

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

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

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2012-09-07T21:59:18.737Z
I think that propositional logic or any other kind of logic would be an answer to the question on surface, but is this what you are looking for?
Tsuyoshi Ito
CC BY-SA 3.0
2012-09-07T22:14:21.423Z
@TsuyoshiIto Prolog is 2-state in a sense that prolog is based on closed world assumption. I'm searching for prolog-like language without CWA. Also I'm interested in methods of counter-example search.
user1123502
CC BY-SA 3.0
2012-09-07T22:23:36.463Z
I am not sure if your comment is meant to be a reply to me, but if so, I fail to see its connection to my comment.  I did not mention Prolog at all.
Tsuyoshi Ito
CC BY-SA 3.0
2012-09-07T23:07:36.257Z
@TsuyoshiIto Yes, you may fail to see connection, because I can not give you an answer to your question. Such an answer to your question will be 80% of an answer to my question. At the same time, I hope, a person, who is familiar with prolog-like-language-without-CWA may easily point out that a sought-for foundations are, say, some observations on the first order logic.
user1123502
CC BY-SA 3.0
2012-09-07T23:19:25.717Z
My question is: Is just answering ‘propositional logic’ a satisfactory answer to you?  I suppose not, but then you are not stating your question precisely enough, because I definitely think that propositional logic is a “theoretical foundation for a three-state Prolog-like language,” if I take this phrase by its face value.
Tsuyoshi Ito
CC BY-SA 3.0
2012-09-07T23:30:17.513Z
@TsuyoshiIto I agree. So please review new edition of my question. UPDATE: may be to remove all the text except the last paragraph?
user1123502
CC BY-SA 3.0
2012-09-07T23:43:02.880Z
I think that the question is much clearer now.  Thanks for the edit.  But: “there are papers that describe such attempts and explore theoretic foundations of such a 3-state prolog-like language”: I do not know what you mean by this sentence.  If you already know such papers exist, what are you asking?
Tsuyoshi Ito
CC BY-SA 3.0
2012-09-07T23:50:19.407Z
Just added "I suspect" second time and made some edits. And again thanks for your review.
user1123502
CC BY-SA 3.0
2012-09-09T01:52:31.267Z
sounds like you want a theorem proving system (ATP) that can attack an undecidable problem (which are similar to propositions that are independent of the axioms). such systems do exist, but am not aware of any that are related to prolog implementations. this paper uses the idea & argues at the end that closed vs open world are somewhat interchangeable.. [open and closed world types in NLP systems by Gerdemann](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.39.387&rep=rep1&type=pdf)
vzn
CC BY-SA 3.0
2016-07-08T14:20:47.860Z
Would the semantic web, OWL and RDF be a candidate? I've read things saying that it tries to use the open world assumption.
CMCDragonkai
<reference-request><soft-question><pl.programming-languages><big-picture><logic-programming>
Papers on Prolog-like languages without closed world assumption (CWA)
user1123502
# Papers on Prolog-like languages without closed world assumption (CWA)

(Asked by: username_0 on 2012-09-07)

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.

**Tags:** reference-request, soft-question, pl.programming-languages, big-picture, logic-programming

> **Comments:**
> **username_1**: I think that propositional logic or any other kind of logic would be an answer to the question on surface, but is this what you are looking for?  
> **username_0**: @TsuyoshiIto Prolog is 2-state in a sense that prolog is based on closed world assumption. I'm searching for prolog-like language without CWA. Also I'm interested in methods of counter-example search.  
> **username_1**: I am not sure if your comment is meant to be a reply to me, but if so, I fail to see its connection to my comment.  I did not mention Prolog at all.  
> **username_0**: @TsuyoshiIto Yes, you may fail to see connection, because I can not give you an answer to your question. Such an answer to your question will be 80% of an answer to my question. At the same time, I hope, a person, who is familiar with prolog-like-language-without-CWA may easily point out that a sought-for foundations are, say, some observations on the first order logic.  
> **username_1**: My question is: Is just answering ‘propositional logic’ a satisfactory answer to you?  I suppose not, but then you are not stating your question precisely enough, because I definitely think that propositional logic is a “theoretical foundation for a three-state Prolog-like language,” if I take this phrase by its face value.  
> **username_0**: @TsuyoshiIto I agree. So please review new edition of my question. UPDATE: may be to remove all the text except the last paragraph?  
> **username_1**: I think that the question is much clearer now.  Thanks for the edit.  But: “there are papers that describe such attempts and explore theoretic foundations of such a 3-state prolog-like language”: I do not know what you mean by this sentence.  If you already know such papers exist, what are you asking?  
> **username_0**: Just added "I suspect" second time and made some edits. And again thanks for your review.  
> **username_2**: sounds like you want a theorem proving system (ATP) that can attack an undecidable problem (which are similar to propositions that are independent of the axioms). such systems do exist, but am not aware of any that are related to prolog implementations. this paper uses the idea & argues at the end that closed vs open world are somewhat interchangeable.. [open and closed world types in NLP systems by Gerdemann](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.39.387&rep=rep1&type=pdf)  
> **username_3**: Would the semantic web, OWL and RDF be a candidate? I've read things saying that it tries to use the open world assumption.  

---

## 1 answers

### Answer by username_4 on 2012-11-13. Score: 4

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](http://www.leancop.de/ileantap/) (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](http://en.wikipedia.org/wiki/Paradigm_shift#Kuhnian_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).

> **Comments:**
> **username_4**: [Computer derives natural laws from raw data](http://www.news.cornell.edu/stories/April09/NaturalLaws.ws.html)--while this project took the essentially opposite, bottom-up from scratch approach: "The researchers found that seeding the complex pendulum problem with terms from equations for the simple pendulum cut processing time to seven or eight hours. This "bootstrapping," they said, is similar to the way human scientists build on previous work." It seems that giving their computer a Prolog-like repository would speed up its heuristics.  

---

