Home » forums » LtU Forum

Inconsistency Robustness in Logic Programs

Inconsistency robustness is “information system performance in the face of continually pervasive inconsistencies.” Inconsistency robustness is both an observed phenomenon and a desired feature:
• It is an observed phenomenon because large information systems are required to operate in an environment of pervasive inconsistency. How are they doing?
• It is a desired feature because we need to improve the performance of large information systems

This paper explores the role of Inconsistency Robustness in the history and theory of Logic Programs. Inconsistency Robustness has been a continually recurring issue in Logic Programs from the beginning including Church's system developed in the early 1930s based on partial functions (defined in the lambda calculus) that he thought would allow development of a general logic without the kind of paradoxes that had plagued earlier efforts by Frege, Russell, etc. Unfortunately, Church's system was quickly shown to be inconsistent because:
• His system allowed the kind of self-referential propositions introduced by Gödel using fixed points on a (implicit) overly loose grammar of mathematical sentences.
• Church thought that a general system must be able to computationally enumerate its theorems
In the face of the contradictions, Church abandoned the quest for a general foundation and subsequently used the lambda calculus solely for the purpose of computation.

[Kowalski 1988] advocated a bold thesis: “Looking back on our early discoveries, I value most the discovery that computation could be subsumed by deduction.” However, mathematical logic cannot always infer computational steps because computational systems make use of arbitration for determining which message is processed next by a recipient that is sent multiple messages concurrently. Since reception orders are in general indeterminate, they cannot be inferred from prior information by mathematical logic alone. Therefore mathematical logic alone cannot in general implement computation. Logic Programs (like Functional Programs) are useful idioms even though they are not universal. For example Logic Programs can provide useful principles and methods for systems which are quasi-commutative and quasi-monotonic even though the systems themselves cannot be implemented using Logic Programs.

According to [Feferman 2008]:"So far as I know, it has not been determined whether such [inconsistency robust] logics account for 'sustained ordinary reasoning', not only in everyday discourse but also in mathematics and the sciences." Direct Logic is put forward as an improvement over classical logic with respect to Feferman’s desideratum above using
• Inconsistency Robust Direct Logic for pervasively inconsistent theories of practice, e.g., theories for climate modeling and for modeling the human brain
• Classical Direct Logic (augmentation of Inconsistency Robust Direct Logic with the rule of Proof by Contradiction) for theories thought to be consistent by an overwhelming consensus of working professional mathematicians
The claim is made that Inconsistency Robust Direct Logic is an improvement over classical logic with respect to Feferman’s desideratum above for today's information systems that are perpetually, pervasively inconsistent. Information technology needs an all-embracing system of inconsistency-robust reasoning to support practical information integration. Having such a system is important in computer science because computers must be able to carry out all inferences (including inferences about their own inference processes) without relying on humans.

Independent developments by different research groups in the fall of 1972 gave rise to a controversy over Logic Programs that persists to this day in the form of following alternatives:
1. Logic Programs using procedural interpretation of program-clause syntax (Logic Programs are Y⇐F1, ..., Fn where Y and each of the Fi is a literal proposition or its negation (i.e., either P[t1, ..., tn] or ¬P[t1, ..., tn] for some atomic predicate P and terms ti.)
2. Logic Programs in which each computational step (e.g. using the Actor Model of computation) is logically inferred (e.g. using Direct Logic)
This article argues for the second alternative based on the following considerations:
• Programs in program-clause syntax are a special case of the second alternative because each computational step of a program in program-clause syntax is logically inferred.
• Reducing propositions to program-clause syntax can obscure their natural structure.
•Procedural interpretation of program-clause syntax does can obscure the natural structure of proofs (e.g. Natural Deduction using Direct Logic).

Consequently, Direct Logic is proposed as a foundation for Logic Programs.

Going beyond the limitations of program-clause syntax, a core subset of Logic Program constructs is presented in this article (using explicit assertions and goals to invoke pattern-directed procedures) that are applicable to both mathematical theories and theories of practice.

The above examples are intended to be case studies in Inconsistency Robustness in which information is formalized, contradictions are derived using Inconsistency Robust reasoning, and arguments are formalized for and against contradictory propositions. A challenge for the future is to automate the reasoning involved in these case studies.

Above abstract is from  the full article

By Hewitt at 2013-11-27 21:17 | LtU Forum | previous forum topic | next forum topic | other blogs | 10445 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Only in logic programming?

Do you want to discuss practical application? As it affects messaging in distributed systems? Your third paragraph implies you think this applies to actual systems that send messages. But if this is actually just about math, I'll back off and keep quiet because I have little patience with abstract formal systems.

Yesterday at lunch I told a coworker that folks exist who think proving things in math can make software better in contexts where otherwise results might be chaotic or poor in quality. I said usually no one addresses the effect of random non-deterministic failures, like message loss or corruption in network contexts, when this affects reasoning about systems receiving and acting upon such messages. Your work sounds like an attempt to deal with this, by improving robustness in the face of inconsistency induced by non-deterministic message processing effects. Just let me know if this isn't so.

However, mathematical logic cannot always infer computational steps because computational systems make use of arbitration for determining which message is processed next by a recipient that is sent multiple messages concurrently. Since reception orders are in general indeterminate, they cannot be inferred from prior information by mathematical logic alone.

Nights and weekends I've been designing a hobby project (thorn) I resumed casually 18 months ago, starting with a post I put up here once in response to a split-stacks/green-threads subthread (Feb 29, 2012), started when you said futures are simpler than promises, and I replied that it depends on thread efficiency. (All those links are to comments in the same page.) I thought I would give it up quickly, but I never did, and now it dominates my background thought process any time I think about coding outside work.

I haven't written anything down yet — just the sort of mental drafting of prose and code interfaces one does when designing how something is supposed to work. (About twenty years ago, I noticed I made slower design progress when coding, when always distracted by what the next bit of code looks like. So large conceptual break-throughs happened only when I became dog sick with the flu, so I could do nothing but think. I expect by not coding yet, I've been keeping the idea alive, because I often find code boring when learning less that's new.) So I have no docs yet for others.

For about the last week I've been reading Plan9 docs, in case imitating parts is a clear way to add a feature. I'm trying to decide whether message passing, as done in the 9P protocol, is instrumental to an effect I need in control flow between lightweight processes. Async data flow with byte streams is easy: clearly modeled by pipes and producer/consumer coroutines with refcounted copy-on-write memory management for immutable functional programming effects. Control-plane behavior via messages is less clear. Consistency is probably a good idea, as opposed to total balkanization from every process rolling its own message scheme. A common (but open and extensible) approach to marshalling and unmarshalling messages can add reflection and centralized tracking to cope with non-deterministic effects, so hiccups are handled robustly.

Thus I have message passing on the brain, and you said something related. Do you have anything to say about message passing? Or is your concern mainly with related math? Something you say could change my plans; that's why I ask. Any insights into what you infer from patterns of messages received? Or is the only form of consistency to be had from implementing Paxos, or something, which I don't care to think about right now.

By Rys McCusker at Thu, 2013-11-28 00:49 | login or register to post comments

Inconsistency Robust Logic Programs is practical

Inconsistency Robust Logic Programs are increasingly becoming immensely practical in higher-level concurrent message passing. As Alan Kay has pointed out, the most important part of object-oriented programs is message passing and not the object hierarchy.

By Hewitt at Thu, 2013-11-28 18:19 | login or register to post comments

okay.

No argument from me there. I am talking about concurrent message passing. And I agree with Kay. An important aspect of actors is replaceability, since what matters is what they say, not how a specific one works.

If concurrent async actors work correctly, it doesn't matter where they are located. So moving them should not change results. Actually moving them in testing is a necessary part of verification. Code should work in the same OS process, or multiple local OS processes, or distributed across remote nodes. When the latter is a goal, being able to test locally is a debugging convenience. Because local usually means more consistent and stable, a fuzzer is needed to simulate remote and poor conditions. A fuzzer is also needed to consistently simulate the same sort of failures, so remote testing actually goes through all edge conditions, despite many being hard to get in practice when systems try so hard to behave reliably instead. All you need is an intermediate actor modeling poor behavior, which understands the same messages, so you can explicitly represent effects you want tested.

I see how you might think I meant something that wasn't concurrent, since most programmers have trouble with concurrency. It would not be worth having a conversation with someone who only knows what an average person does. A venue with a lot of activity and participants would work better for that.

By Rys McCusker at Thu, 2013-11-28 20:55 | login or register to post comments

Concurrent message passing is fundamental to Computer Science

Yes indeed, concurrent message passing is fundamental to Computer Science. And it needs to work regardless of whether the Actor being sent a message is local, non-local, or in transit between machines.

By Hewitt at Fri, 2013-11-29 17:57 | login or register to post comments

Alas, poor Yorick.

Concurrent message passing represents signal propagation, which is inescapable in hardware and therefore fundamental, yes. As a picture, you might draw it as an arrow -event-> where the event is a message. But term event usually means a user interface message like key-down or mouse-down to most programmers, despite this being useful as a more general idea too. We might use acronym EOP for event oriented programming for "concurrent message passing", which I'm not going to write again because life is too short for seven syllables. :-) Acronym CMP usually means concurrent multi-processing, which is related, while EDP usually means event driven programming, normally narrowed to mean only OS event handling rather than messages in general, so we should avoid that. (Wikipedia links related topic signal programming, which does note the more general idea.)

When I googled for "event oriented programming", I found someone with handle Poor Yorick, a fellow of infinite jest, describes EOP as follows at http://www2.tcl.tk/1772 in a summary. Since this agrees with what I wanted that phrase to mean, I include it here for color:

Although similar in some ways to the idea of concurrency, event-driven programming is a strategy for designing the control flow of a program which must react to events that are external to the program itself. Such programs may use threads, coroutines, continuations, generators, and other facilities to accomplish the goal of processing external events.

If I were you, I'd promote term eo as event-oriented, because it's also the irregular Latin verb for to go, which fits the arrow idea nicely. It's at least as useful an idea as object- or aspect-oriented.

I sometimes mention my thorn hobby project to a guy at work who did high availability work at Tandem in a previous life (high end stock market signal handling), and he's really keen on the idea of events and message passing as central to better results when you want predictable behavior. For example, when I described my approach to handle Unix style signals in lightweight processes, he said I wanted to turn them into events, and I replied that was what I just said. (If it's one of the standard signals, set a bit and awaken the lightweight thread fiber that handles messages. The bit is the message. McLuhan didn't say that, though.) Plan9 calls signals notes and uses them for notification. Same idea.

I actually started writing this to reply to the following part of your pleasant, though brief, response:

... or in transmit between machines.

By moving actors, I actually meant running a test again with a new configuration that puts actors elsewhere, for comparison to an earlier test. What you said is correct, that should work too—moving an actor between machines—but implies an expensive message handling infrastructure that can store-and-forward over a location change hiatus. Folks from the New Jersey school of worse-is-better would never do this. Instead you might get an error when the original location was now vacated. However, if you really were going to make a distributed app that migrated actors, and you wanted to guarantee delivery, then your version follows as necessary. But it's very hard to get devs and managers to commit to guarantees, unless customers with checkbooks have such in their checklists that gate purchase.

Edit: the rest of this is a fictional dialog about signal bitflags and message handling in a lightweight process, and is mostly off-topic because it doesn't shed much light on concurrent message passing. Rather, it addresses confusion in folks who hear an operating system term used, then assume all OS semantics are necessarily relevant when this is immaterial.

     "That doesn't sound secure," Ned worried. "Anyone could set a bit for a signal. What about defense against evil intent? Do you need a permission system?"
     "Also, can you add the evil-bit from RFC3514 to messages?" Crash wondered aloud with a hint of smile. "That way you can just ignore bad input so annotated."
     "Funny," Wil granted, then turned to Ned. "When you put a thread pool inside your app, how do you protect against evil intent in code you put in other threads? It's all your own code. You can step on memory with pointers in C; why bother expressing evil with a signal bit? There's no memory protection among lanes in one OS process anyway."
     "What's a lane again?" Dex interrupted.
     "Wil's term for a lightweight process," Ned explained. "Term process only refers to an OS process that way. Less confusing."
     "Suppose you write a prototype with a few OS processes," Wil continued. "Maybe you use signals to coordinate. When you move this into a coroutine scheduler as fiber lanes, you can use the same signals, but now it's cooperative like all other fiber behavior. Use signals or not, I don't care."
     "Is it a complete free-for-all then?" Dex asked with a dubious look.
     "You say that like it's a bad thing," Crash noted.
     "Yes," Wil nodded, "just like all your other C code is a free-for-all, letting any function call any other, as you like. Lanes and fibers are just cooperative organization, and just like when using threads, you can still shoot yourself in the foot any time you want. Just don't do that."
     "Okay, I get it now," Ned waved to say his question was answered. "I both send signals and handle them: don't confuse myself."

By Rys McCusker at Fri, 2013-11-29 21:24 | login or register to post comments

Kowalski

In contrast with previous work, Kowalski has advocated limiting Logic Programming to backward-chaining only inference based on unit resolution. However, his proposal leaves out forward chaining and other logical operations.

Do you have a reference for that? I ask this since the latest book I read of his, Computational Logic and Human Thinking from 2011, mentions both forward- and backward-chaining, both of these being fundamental to his model for computational logic. I've not read anything of his more recent than this book.

By Barry Watson at Thu, 2013-11-28 05:49 | login or register to post comments

Kowalski's advocacy of Logic Programs

Kowalski originally advocated Logic Programs using backward chaining, unlike previous work, e.g., Planner. However, as you point out, in his latest book he also allows AI-like production systems that do forward-chaining. However, [Kowalski 2011] did not classify these production systems as Logic Programs. Furthermore, there are other logical operations not included in Kowalski's version of Logic Programs, e.g., type inference.

P.S. There are extensive references and further discussion in the article linked at the beginning of this forum topic.

By Hewitt at Thu, 2013-11-28 18:13 | login or register to post comments

Combining forward and back chaining in Logic Programs

Forward chaining and backward chaining can be combined in Logic Programs as follows:

Forward chaining: when (⊢Φ), ⊢(Φ⊢Ψ) → ⊢Ψ

Backward chaining: when (||- Ψ), ⊢(Φ⊢Ψ) → ||- Φ

See the article linked at the beginning of this forum topic for an explanation of the notation used in the above examples.

By Hewitt at Sat, 2013-11-30 12:55 | login or register to post comments

Removed

Removed

By j4n bur53 at Sat, 2013-11-30 13:26 | login or register to post comments

Removed

Removed

By j4n bur53 at Sat, 2013-11-30 18:44 | login or register to post comments

||- means "goal" (originated in Planner)

||- means "goal" (which originated in Planner).

For example, consider the following:

Backward chaining: when (||- Ψ), ⊢(Φ⊢Ψ) → ||- Φ

which means

Backward chaining: when Ψ is a goal and (Φ⊢Ψ) is an assertion, make Φ a goal

By Hewitt at Sat, 2013-11-30 20:34 | login or register to post comments

Removed

Removed

By j4n bur53 at Sat, 2013-11-30 22:30 | login or register to post comments

Removed

Removed

By j4n bur53 at Fri, 2013-11-29 19:21 | login or register to post comments

Resolution proving is assume opposite and derive contradiction

Resolution theorem proving is to assume opposite of what is to be proved and derive a contradiction. Consequently, in resolution theorem proving:

Backward chaining from goal G is to add ¬G to database and prefer resolving on G and its resolvents until a contradiction is obtained: a proof procedure that is complete, although enormously inefficient in practice to the point of being unworkable. Planner amounted to a rejection of the Resolution Uniform Poof Procedure Paradigm and a proposal to adopt Procedural Embedding as an alternative.

Kowalski did not allow forward chaining in Logic Programs in part because forward chaining does not fit within the resolution theorem proving paradigm:

To forward chain from proposition P, you might try adding P to database and prefer resolving on P and its resolvents: a proof procedure that is not complete in deriving conclusions from P!

PS. You might try reading the full article (i.e., not just the abstract) before adding insults to your comments.

By Hewitt at Fri, 2013-11-29 20:05 | login or register to post comments

Removed

Removed

By j4n bur53 at Fri, 2013-11-29 21:16 | login or register to post comments

Prolog backward chaining was based on goal-preference resolution

Prolog backward chaining was based on goal-preference resolution in the sense of adding the negation of a goal to the data base and preferring resolution with the negation of the goal and its resolvents. In first-order logic, adding the negation of a goal to a consistent database is inconsistent if and only if the goal is provable from the database.

By Hewitt at Fri, 2013-11-29 21:42 | login or register to post comments

Removed

Removed

By j4n bur53 at Fri, 2013-11-29 21:59 | login or register to post comments

Removed

Removed

By j4n bur53 at Fri, 2013-11-29 22:17 | login or register to post comments

Cut elimination with lemma reuse

See for example the work by some folks from CMU and elsewhere. Its actually not so difficult. You just combine some rules from a cut eliminated minimal logic calculus in a certain way and you get both forward and backward chaining.

Do you recommend any specific papers for this?

What I like about the forward chaining in cut eliminated proofs, is basically that it shows that also cut eliminated proofs can have lemma reuse.

I've recently been planning out a couple of programming languages that have multiple stages to their semantics. Early stages pave a road for later stages to drive on. Right now, the early stages just inline every abstraction, but I'd rather find a way for the outcome to be easier to understand and less bloated with redundancy. It sounds like that kind of cut elimination could come in handy!

By Ross Angle at Fri, 2013-11-29 23:11 | login or register to post comments

Removed

Removed

By j4n bur53 at Sat, 2013-11-30 01:04 | login or register to post comments

Re: Removed

Removed

Well, I certainly appreciated this subthread in particular. :) Thank you for giving me a sense of the difference between 1) doing cut elimination and 2) working in a cut-eliminated calculus.

The larger discussion about forward chaining, polarity, and assertions-vs.-goals was also very interesting. I had already been thinking about the backwards-and-forwards computation of linear types, continuations, constraint solving, and type inference, so this discussion was some nice food for thought. The other day, I took a brief look at attribute grammars and appreciated their backwards-and-forwards propagation in a new light.

Thanks for bringing out so much depth despite the responses you've been getting, and it's not surprising if you're exasperated.

By Ross Angle at Tue, 2013-12-31 01:10 | login or register to post comments

Focusing, focusing, focusing

(I keep opening tabs on those annoying threads just because I am more comfortable when there is nothing with a red star in the 'recent posts' page. Countably Infinite has a gift for creating interesting discussion islands; thanks for the reference on pedagogical logic.)

See for example the work by some folks from CMU and elsewhere. Its actually not so difficult. You just combine some rules from a cut eliminated minimal logic calculus in a certain way and you get both forward and backward chaining.

There is an entire subdomain of logic working on using focusing to control the dynamics of proof search. Focusing proposes a distinction between "interesting" and "boring" proof steps (those that are "inversible" and can be done at any moment are boring, the important ones are those that destroy some information).

Some formulas/constructors are only interesting when you try to prove them ("on the right") and are said "positive", some are only interesting when you try to use them ("on the left") and are said "negative", and for some of them (such as atoms, or possibly "product" in intuitionistic logic (as opposed to linear) where negative and positive products are equivalent provability-wise) you have a choice. You can assign the latter a "polarity", which corresponds to deciding in advance whether you want to use them negatively or positively.

It is now well-known that polarization strategies (the way you decide polarities) correspond to rather precise choice of dynamics of proof search. If you force all atoms to be "negative", they will be "built on the left", that is asserted once they become provable from the context (independently of the goal), so you have forward chaining. If you force all atoms to be "positive", they will be used when they appear "on the right", in a goal, so you have backward chaining. A Logical Characterization of Forward and Backward Chaining in the Inverse Method, by Kaustuv Chaudhuri, Frank Pfenning and Greg Price, 2007.

And that's only the beginning, as "all negative" and "all positive" are a very coarse way to control dynamics. Define the calculus in just the right way, choose just the right polarization strategy, and you get a proof search bisimilar to DPLL (M. Farooque, S. Graham-Lengrand and A. Mahboubi, 2013). Or decide to change the polarity of the atoms dynamically, and you can emulate Magic Sets (Kaustuv Chaudhuri, 2010).

By gasche at Sat, 2013-11-30 14:11 | login or register to post comments

Removed

Removed

By j4n bur53 at Sat, 2013-11-30 23:11 | login or register to post comments

Removed

Removed

By j4n bur53 at Fri, 2013-11-29 21:43 | login or register to post comments

Forward chaining using resolution rule is not complete

Forward chaining using the resolution rule is not complete.

For example, consider the following database:

Switch[On]∎
Lamp[Off]∎
Battery[Empty] ∨ ¬Switch[On] ∨ ¬Lamp[Off]∎

From the above database, the following cannot be proved by forward chaining using the resolution rule even though they are consequences in first-order logic:

Switch[On] ∨ Lamp[On]∎
Lamp[On] ∨ ¬Lamp[On]∎

Of course, each of the above can be proved using backward chaining by putting its negation in the data base and then deriving a contradiction using the resolution rule.

By Hewitt at Sat, 2013-11-30 04:42 | login or register to post comments

Removed

Removed

By j4n bur53 at Sat, 2013-11-30 10:04 | login or register to post comments

Control question

Hi Carl

I would like to know more about the so called "control problem" back in your Planner days at MIT. If this makes any sense at all could you explain it a little. Control theory at that time was going through a revolution, but I had the feeling then and in later years that it was not going over very well, not only outside electrical engineering but even within electrical engineers. The reaction against dynamic programming and state in Lisp programming seems to be related or at least coincident with the explosion of new knowledge in control. There is also an obvious link to forward chaining and Actors.

Reference: Hairy control.
Any information would be appreciated.
Thanks

By Hank Thediek at Mon, 2013-12-02 12:47 | login or register to post comments

Removed

Removed

By j4n bur53 at Tue, 2013-12-03 12:26 | login or register to post comments

Logic Programs development illustrates Inconsistency Robustness

The development of Logic Programs illustrates fundamental issues in Inconsistency Robustness. Contradictions were endemic in the development of Logic Programs. How were they addressed?

See the article linked in the post at the beginning of this forum topic.

By Hewitt at Tue, 2013-12-03 18:23 | login or register to post comments

nowt.

But taking PLANNER as an attack against the novelity
of Prolog is new to me.

The first two papers in Implementations of PROLOG discuss MICRO-PLANNER and POPLER (a POP-2 based PLANNER). It seems that back in 1984, PLANNER-like languages were considered part of Prolog's history by some.
According to the book, the key notions of MICRO-PLANNER were goal orientation, procedural embedding of knowledge, a system maintained database, pattern directed invocation, and backtracking. I must say that looks very much like Prolog. Then again, they were describing it in a book for Prolog implementers.

From my quick reading I reckon


(PROG () (OR (GOAL (G1))
             (GOAL (G2))
             (GOAL (G3)))
          (FAIL))

should be roughly equivalent to


(g1; g2; g3), fail.

I just made that example up using an example in the paper, so it's probably wrong. Considering s-expressions are really abstract syntax it's pretty much the same thing.

The attack is rather on the
phenotype of Prolog than on the genotype of Prolog.
What can be gained from such an attack?

Not much I reckon. Prolog's place in history has been set in stone.

Doesn't the Marseille genotype explain the
existence of definite clause grammars (DCGs) in Prolog.

According to A Grammatical View of Logic Programming, Deransart and Maluszynski:

Historically, the notion of DCG originates from Colmerauer's notion of metamorphosis grammar

So yes it looks like it does.

By Barry Watson at Tue, 2013-12-03 19:27 | login or register to post comments

Prolog developed as a backward chaining subset of Micro-Planner

Prolog development by Kowalski was from Micro-Planner according to the references quoted in the article linked at the beginning of this forum topic. The decision have Prolog perform only backward chaining was influenced by grammatical work of Colmerauer.

However, the development of Logic Programs goes back to [Jaśkowski 1934] and [Church 1936].

By Hewitt at Tue, 2013-12-03 19:41 | login or register to post comments

Removed

Removed

By j4n bur53 at Wed, 2013-12-04 08:53 | login or register to post comments

Future of Logic Programs is many-core concurrency

The future of Logic Programs is many-core concurrency :-)

By Hewitt at Wed, 2013-12-04 16:22 | login or register to post comments

Removed

Removed

By j4n bur53 at Wed, 2013-12-04 17:59 | login or register to post comments

Prolog does not concurrently backward and forward chain :-(

Prolog does not concurrently backward and forward chain :-(

By Hewitt at Wed, 2013-12-04 18:18 | login or register to post comments

Removed

Removed

By j4n bur53 at Wed, 2013-12-04 20:24 | login or register to post comments

Prolog doesn't even have mechanism for concurrent inference

Prolog doesn't even have required mechanism for concurrent inference, e.g., it lacks both ⊢ for assertions and ||- for goals.

By Hewitt at Thu, 2013-12-05 15:49 | login or register to post comments

Removed

Removed

By j4n bur53 at Thu, 2013-12-05 19:01 | login or register to post comments

Control structure issues in theorem proving

Hi Hank,

Control structure has been an important issue in computer theorem proving ever since McCarthy's Advice Taker and the Newell, Shaw, and Simon Logic Theorist. As discussed the article linked at the beginning of this forum topic, Prolog duplicated many of the control structure limitations of Micro-Planner (partly because of the same hardware limitations at the time).

Cheers,
Carl

By Hewitt at Mon, 2013-12-02 13:17 | login or register to post comments

Removed

Removed

By j4n bur53 at Thu, 2013-12-05 19:32 | login or register to post comments

Removed

Removed

By j4n bur53 at Thu, 2013-12-05 22:38 | login or register to post comments

Negation as failure (from Planner): ||- (¬⊢p) → ⊢¬p

Negation as failure (originated in Planner) can formalized as follows:

||- (¬⊢p) → ⊢¬p

By Hewitt at Fri, 2013-12-06 03:55 | login or register to post comments

Removed

Removed

By j4n bur53 at Fri, 2013-12-06 04:55 | login or register to post comments

Negation as Failure: less proveable means more can be asserted!

The use of Negation as Failure gave rise to the following joke: The less a Planner program can prove, the more it can assert using Negation as Failure!

By Hewitt at Fri, 2013-12-06 06:18 | login or register to post comments

Removed

Removed

By j4n bur53 at Fri, 2013-12-06 08:36 | login or register to post comments

Logic Programs should be monotonic for assertions and goals

Logic Programs should be monotonic for both assertions (⊢) and goals (||-).

By Hewitt at Fri, 2013-12-06 15:55 | login or register to post comments

Removed

Removed

By j4n bur53 at Fri, 2013-12-06 21:56 | login or register to post comments