Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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.

share|improve this question
    
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 Sep 7 '12 at 21:59
    
@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 Sep 7 '12 at 22:14
    
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 Sep 7 '12 at 22:23
    
@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 Sep 7 '12 at 23:07
    
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 Sep 7 '12 at 23:19
show 5 more comments

1 Answer

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).

share|improve this answer
    
Computer derives natural laws from raw data--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 Nov 13 '12 at 17:24
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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