Development of Logic Programming: What went wrong, What was done about it, and What it might mean for the future

Logic Programming can be broadly defined as “using logic to deduce computational steps from existing propositions” (although this is somewhat controversial). The focus of this paper is on the development of this idea. Consequently, it does not treat any other associated topics related to Logic Programming such as constraints, abduction, etc.

The idea has a long development that went through many twists in which important questions turned out to have surprising answers including the following:

• Is computation reducible to logic?

• Are the laws of thought consistent?

This paper describes what went wrong at various points, what was done about it, and what it might mean for the future of Logic Programming.

The paper can be found at Development of Logic Programming: What went wrong, What was done about it, and What it might mean for the future.

Common sense for concurrency and strong paraconsistency using unstratified inference and reflection

This paper develops a very powerful formalism (called Direct Logic™) that incorporates the mathematics of Computer Science and allows unstratified inference and reflection using mathematical induction for almost all of classical logic to be used. Direct Logic allows mutual reflection among the code, documentation, and use cases of large software systems thereby overcoming the limitations of the traditional Tarskian framework of stratified metatheories.

Gödel first formalized and proved that it is not possible to decide all mathematical questions by inference in his 1st incompleteness theorem. However, the incompleteness theorem (as generalized by Rosser) relies on the assumption of consistency! This paper proves a generalization of the
Gödel/Rosser incompleteness theorem: a strongly paraconsistent theory is incomplete. However, there is a further consequence: Although the semi-classical mathematical fragment of Direct Logic is evidently consistent, since the Gödelian paradoxical proposition is self-provable, every reflective strongly paraconsistent theory in Direct Logic is inconsistent!

This paper also proves that Logic Programming is not computationally universal in that there are concurrent programs for which there is no equivalent in Direct Logic. Thus the Logic Programming paradigm is strictly less general than the Procedural Embedding of Knowledge paradigm.

PDF copy of the paper can be downloaded at: Common sense for concurrency and strong paraconsistency using unstratified inference and reflection

Norms and Commitment for ORGs (Organizations of Restricted Generality): Strong Paraconsistency and Participatory Behavioral Model Checking

Organizations of Restricted Generality (ORGs) raise important issues for
commitment, norms, strong paraconsistency and model checking that require
extensions and revisions of previous foundational work.

For example, extension and revision is required of the fundamental assumption of the Event Calculus: Time-varying properties hold at particular time-points if they have been initiated by an action at some earlier time-point, and not terminated by another action in the meantime. The fundamental assumption of the Event Calculus is overly simplistic when it comes to organizations in which time-varying properties have to be actively maintained and managed in order to continue to hold and termination by another action is not required for a property to no longer hold. I.e., if active measures are not taken then things will go haywire by default. Consequently the Event Calculus approach must evolve into a strongly paraconsistent system structured around participations in space-time.

Similarly extension and revision is required for Model Checking properties of systems. Previously Model Checking as been performed using the model of nondeterministic automata based on states determined by time-points. These nondeterministic automata are not suitable for organizations, which are highly structured and operate asynchronously with only loosely bounded nondeterminism. Consequently Model Checking needs to evolve in the direction of verifying participatory behavior in Organizations.

PDF copy of the paper can be downloaded at: Norms and Commitment for ORGs (Organizations of Restricted Generality): Strong Paraconsistency and Participatory Behavioral Model Checking

Large-scale Organizational Computing requires Unstratified Reflection and Strong Paraconsistency

Organizational Computing is a computational model for using the principles, practices, and methods of human organizations. Organizations of Restricted Generality (ORGs) have been proposed as a foundation for Organizational Computing. ORGs are the natural extension of Web Services, which are rapidly becoming the overwhelming standard for distributed computing and application interoperability in Organizational Computing. The thesis of this paper is that large-scale Organizational Computing requires reflection and strong paraconsistency for organizational practices, policies, and norms.

Strong paraconsistency is required because the practices, policies, and norms of large-scale Organizational Computing are pervasively inconsistent. By the standard rules of logic, anything and everything can be inferred from an inconsistency, e.g., “The moon is made of green cheese.” The purpose of strongly paraconsistent logic is to develop principles of reasoning so that irrelevances cannot be inferred from the fact of inconsistency while preserving all natural inferences that do not explode in the face of inconsistency.

Reflection is required in order that the practices, policies, and norms can mutually refer to each other and make inferences. Reflection and strong paraconsistency are important properties of Direct Logic [Hewitt 2007] for large software systems. Gödel first formalized and proved that it is not possible to decide all mathematical questions by inference in his 1^st incompleteness theorem. But the incompleteness theorem (as generalized by Rosser) relies on the assumption of consistency! This paper proves a generalization of the Gödel/Rosser incompleteness theorem: theories of Direct Logic are incomplete. However, there is a further consequence. Although the semi-classical mathematical fragment of Direct Logic is evidently consistent, since the Gödelian paradoxical proposition is self-provable, every theory in Direct Logic has an inconsistency!

The published paper with the above abstract appears in the excellent Springer LNCS volume Coordination, Organizations, Institutions, and Norms in Agent Systems III (edited by Jaime Sichman, Pablo Noriega, Julian Padget and Sascha Ossowski) and can be found at SpringerLink.
A version with some typos corrected is here: Large-scale Organizational Computing requires Unstratified Reflection and Strong Paraconsistency.

ORGs (Organizations of Restricted Generality): Strong Paraconsistency and Participatory Behavioral Model Checking

Organizations of Restricted Generality (ORGs) raise important issues for
commitment, norms, strong paraconsistency and model checking that require
extensions and revisions of previous foundational work.

For example, extension and revision is required of the fundamental assumption of the Event Calculus: Time-varying properties hold at particular time-points if they have been initiated by an action at some earlier time-point, and not terminated by another action in the meantime. The fundamental assumption of the Event Calculus is overly simplistic when it comes to organizations in which time-varying properties have to be actively maintained and managed in order to continue to hold and termination by another action is not required for a property to no longer hold. I.e., if active measures are not taken then things will go haywire by default. Consequently the Event Calculus approach must evolve into a strongly paraconsistent system structured around participations in space-time.

Similarly extension and revision is required for Model Checking properties of systems. Previously Model Checking as been performed using the model of nondeterministic automata based on states determined by time-points. These nondeterministic automata are not suitable for organizations, which are highly structured and operate asynchronously with only loosely bounded nondeterminism. Consequently Model Checking needs to evolve in the direction of verifying participatory behavior in Organizations.

PDF copy of the paper can be downloaded at: ORGs (Organizations of Restricted Generality): Strong Paraconsistency and Participatory Behavioral Model Checking

Middle History of Logic Programming

Logic Programming can be broadly defined as “using logic to deduce computational steps from existing propositions” (although this is somewhat controversial). The focus of this article is on the development of this idea. Consequently, it does not treat any other associated topics related to Logic Programming such as constraints, abduction, etc.

The idea has a long development that went through many twists in which important questions turned out to have surprising answers including the following:

• Is computation reducible to logic?
• Are the laws of thought consistent?

Logic Programming was used as the foundation of the Japanese Fifth Generation Computing Project (ICOT) and was a principle cause of the failure of the project.

Continuation of this article can be found at the following location: Middle History of Logic Programming

Carl Hewitt Articles and Sites

Articles

• see History of Logic Programming for further information.
• see Logical Necessity of Inconsistency for further information.
  

Sites

• see Carl Hewitt on Citizendium for further information
  
• see Carl Hewitt on Windows Live for further information.
• see Carl Hewitt on WordPress for further information.
• see Carl Hewitt on LiveJournal for further information.
• see Carl Hewitt on Blog.com for further information
• see Carl Hewitt on Bloglines for further information.
• see Carl Hewitt on Yahoo for further information.
• see Carl Hewitt on TypePad for further information.

Carl Hewitt's Seminars

See Carl Hewitt Seminars for further information.

Carl Hewitt's Academic Biography

See Carl Hewitt Academic Biography for further information.