The relation between logic programming and logic specification

1984 ◽  
Vol 312 (1522) ◽  
pp. 345-361 ◽  
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Programming Language ◽  
Specification Language ◽  
Formal Logic ◽  
Automated Deduction ◽  
Logic Programs ◽  
Computing Science ◽  
Complete Specification ◽  
Representation Of Knowledge

Formal logic is widely accepted as a program specification language in computing science. It is ideally suited to the representation of knowledge and the description of problems without regard to the choice of programming language. Its use as a specification language is compatible not only with conventional programming languages but also with programming languages based entirely on logic itself. In this paper I shall investigate the relation that holds when both programs and program specifications are expressed in formal logic. In many cases, when a specification completely defines the relations to be computed, there is no syntactic distinction between specification and program. Moreover the same mechanism that is used to execute logic programs, namely automated deduction, can also be used to execute logic specifications. Thus all relations defined by complete specifications are executable. The only difference between a complete specification and a program is one of efficiency. A program is more efficient than a specification.

A PROOF PROCEDURE FOR TEMPORAL LOGIC PROGRAMMING

2004 ◽  
Vol 15 (02) ◽  
pp. 417-443 ◽  
Author(s):  
MANOLIS GERGATSOULIS ◽  
CHRISTOS NOMIKOS
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Temporal Logic ◽  
Programming Language ◽  
Branching Time ◽  
Logic Programs ◽  
Temporal Logic Programming ◽  
Time Logic ◽  
Proof Procedure ◽  
Resolution Proof

In this paper, we propose a new resolution proof procedure for the branching-time logic programming language Cactus. The particular strength of the new proof procedure, called CSLD-resolution, is that it can handle, in a more general way, open-ended queries, i.e. goal clauses that include atoms which do not refer to specific moments in time, without the need of enumerating all their canonical instances. We also prove soundness, completeness and independence of the computation rule for CSLD-resolution. The new proof procedure overcomes the limitations of a family of proof procedures for temporal logic programming languages, which were based on the notions of canonical program and goal clauses. Moreover, it applies directly to Chronolog programs and it can be easily extended to apply to multi-dimensional logic programs as well as to Chronolog(MC) programs.

scholarly journals Theoretical foundations of the organization of branches and repetitions in programs in the logic programming language Prolog

2021 ◽  
Vol 21 (2) ◽  
pp. 200-206
Author(s):  
D. V. Zdor
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Programming Language ◽  
Educational Process ◽  
Prolog Program ◽  
Logic Programming Language ◽  
Technological Basis ◽  
Program Testing ◽  
Logical Language ◽  
Logical Programming

Introduction. The organization of branches and repetitions in the context of logical programming is considered by an example of the Prolog language. The fundamental feature of the program in a logical programming language is the fact that a computer must solve a problem by reasoning like a human. Such a program contains a description of objects and relations between them in the language of mathematical logic. At the same time, the software implementation of branching and repetition remains a challenge in the absence of special operators for the indicated constructions in the logical language. The objectives of the study are to identify the most effective ways to solve problems using branching and repetition by means of the logic programming language Prolog, as well as to demonstrate the results obtained by examples of computational problems.  Materials and Methods. An analysis of the literature on the subject of the study was carried out. Methods of generalization and systematization of knowledge, of the program testing, and analysis of the program execution were used.  Results. Constructions of branching and repetition organization in a Prolog program are proposed. To organize repetitions, various options for completing a recursive cycle when solving problems are given.  Discussion and Conclusions. The methods of organizing branches and repetitions in the logic programming language Prolog are considered. All these methods are illustrated by examples of solving computational problems. The results obtained can be used in the further development of the recursive predicates in logical programming languages, as well as in the educational process when studying logical programming in the Prolog language. The examples of programs given in the paper provide using them as a technological basis for programming branches and repetitions in the logic programming language Prolog.

scholarly journals Generalizations of Rice's Theorem, Applicable to Executable and Non-Executable Formalisms

10.29007/jnl6 ◽  
2018 ◽  
Author(s):  
Cornelis Huizing ◽  
Ruurd Kuiper ◽  
Tom Verhoeff
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Specification Language ◽  
Partial Function ◽  
Program Text ◽  
Turing Machines ◽  
Partial Functions ◽  
Executable Specification ◽  
Special Cases ◽  
Diagonal Argument

We formulate and prove two Rice-like theoremsthat characterize limitations on nameability of propertieswithin a given naming scheme for partial functions.Such a naming scheme can, but need not be, an executable formalism.A programming language is an example of an executable naming scheme,where the program text names the partial function it implements.Halting is an example of a propertythat is not nameable in that naming scheme.The proofs reveal requirements on the naming schemeto make the characterization work.Universal programming languages satisfy these requirements,but also other formalisms can satisfy them.We present some non-universal programming languagesand a non-executable specification languagesatisfying these requirements.Our theorems haveTuring's well-known Halting Theorem and Rice's Theorem as special cases,by applying them to a universal programming language or Turing Machines as naming scheme.Thus, our proofs separate the nature of the naming scheme(which can, but need not, coincide with computability) from the diagonal argument.This sheds further light on how far reaching and simple the `diagonal' argument is in itself.

Constructive mathematics and computer programming

1984 ◽  
Vol 312 (1522) ◽  
pp. 501-518 ◽  
Keyword(s):  
Computer Science ◽  
Programming Languages ◽  
Programming Language ◽  
Program Synthesis ◽  
Constructive Mathematics ◽  
Inference Rules ◽  
Computing Science ◽  
Intuitionistic Theory ◽  
The Difference ◽  
Correct Program

If programming is understood not as the writing of instructions for this or that computing machine but as the design of methods of computation that it is the computer’s duty to execute (a difference that Dijkstra has referred to as the difference between computer science and computing science), then it no longer seems possible to distinguish the discipline of programming from constructive mathematics. This explains why the intuitionistic theory of types (Martin-Lof 1975 In Logic Colloquium 1973 (ed. H. E. Rose & J. C. Shepherdson), pp. 73- 118. Amsterdam: North-Holland), which was originally developed as a symbolism for the precise codification of constructive mathematics, may equally well be viewed as a programming language. As such it provides a precise notation not only, like other programming languages, for the programs themselves but also for the tasks that the programs are supposed to perform. Moreover, the inference rules of the theory of types, which are again completely formal, appear as rules of correct program synthesis. Thus the correctness of a program written in the theory of types is proved formally at the same time as it is being synthesized.

MODULARITY AND CORRECTNESS FOR LOGIC PROGRAMS AND KNOWLEDGE BASES

1994 ◽  
Vol 04 (02) ◽  
pp. 257-275
Author(s):  
GRIGORIS ANTONIOU
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Formal Semantics ◽  
Knowledge Bases ◽  
Algebraic Specification ◽  
Equational Logic ◽  
Logic Programs ◽  
Horn Logic ◽  
Large Systems ◽  
The One

A modularity concept for structuring and developing large logic programs and logical knowledge bases is presented. The concept is motivated from work in the field of algebraic specification, and enforces an extreme modularity discipline that goes beyond the one found in imperative or logic programming languages. As concrete programming languages (respectively knowledge representation formalisms), we consider Horn logic and equational logic programming. We give formal semantics for single modules and discuss correctness and verification issues. Large systems are constructed as interconnections of single modules. We introduce the so-called module operations of composition, actualization, and union, and give results concerning compositionality of semantics and correctness preservation.

Knowledge Representation to Empower Expert Systems

2011 ◽  
pp. 576-583
Author(s):  
James D. Jones
Keyword(s):  
Knowledge Representation ◽  
Expert Systems ◽  
Logic Programming ◽  
Programming Languages ◽  
Default Reasoning ◽  
Logic Programs ◽  
Specific Domain ◽  
Negation As Failure ◽  
Complex Forms ◽  
Representation Scheme

Knowledge representation is a field of artificial intelligence that has been actively pursued since the 1940s.1 The issues at stake are that given a specific domain, how do we represent knowledge in that domain, and how do we reason about that domain? This issue of knowledge representation is of paramount importance, since the knowledge representation scheme may foster or hinder reasoning. The representation scheme can enable reasoning to take place, or it may make the desired reasoning impossible. To some extent, the knowledge representation depends upon the underlying technology. For instance, in order to perform default reasoning with exceptions, one needs weak negation (aka negation as failure. In fact, most complex forms of reasoning will require weak negation. This is a facility that is an integral part of logic programs but is lacking from expert system shells. Many Prolog implementations provide negation as failure, however, they do not understand nor implement the proper semantics. The companion article to this article in this volume, “Logic Programming Languages for Expert Systems,” discusses logic programming and negation as failure.

scholarly journals Implementing a Library for Probabilistic Programming Using Non-strict Non-determinism

2019 ◽  
Vol 20 (1) ◽  
pp. 147-175 ◽  
Author(s):  
SANDRA DYLUS ◽  
JAN CHRISTIANSEN ◽  
FINN TEEGEN
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Programming Language ◽  
Probabilistic Choice ◽  
Probabilistic Programming ◽  
Logic Programming Language ◽  
Functional Logic Programming ◽  
Functional Logic ◽  
Language Characteristics ◽  
Standard List

AbstractThis paper presentsPFLP, a library for probabilistic programming in the functional logic programming language Curry. It demonstrates how the concepts of a functional logic programming language support the implementation of a library for probabilistic programming. In fact, the paradigms of functional logic and probabilistic programming are closely connected. That is, language characteristics from one area exist in the other and vice versa. For example, the concepts of non-deterministic choice and call-time choice as known from functional logic programming are related to and coincide with stochastic memoization and probabilistic choice in probabilistic programming, respectively. We will further see that an implementation based on the concepts of functional logic programming can have benefits with respect to performance compared to a standard list-based implementation and can even compete with full-blown probabilistic programming languages, which we illustrate by several benchmarks.

The language of epistemic specifications (refined) including a prototype solver

2015 ◽  
Vol 30 (4) ◽  
pp. 953-989 ◽  
Author(s):  
Patrick Kahl ◽  
Richard Watson ◽  
Evgenii Balai ◽  
Michael Gelfond ◽  
Yuanlin Zhang
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Epistemic Logic ◽  
Formal Semantics ◽  
Logic Program ◽  
Logic Programs ◽  
Logic Programming Language ◽  
Conformant Planning

Abstract In this article, we present a new version of the language of Epistemic Specifications. The goal is to simplify and improve the intuitive and formal semantics of the language. We describe an algorithm for computing solutions of programs written in this new version of the language. The new semantics is illustrated by a number of examples, including an Epistemic Specifications-based framework for conformant planning. In addition, we introduce the notion of an epistemic logic program with sorts . This extends recent efforts to define a logic programming language that includes the means for explicitly specifying the domains of predicate parameters. An algorithm and its implementation as a solver for epistemic logic programs with sorts is also discussed.

scholarly journals A Linear Logic Programming Language for Concurrent Programming over Graph Structures

2014 ◽  
Vol 14 (4-5) ◽  
pp. 493-507 ◽  
Author(s):  
FLAVIO CRUZ ◽  
RICARDO ROCHA ◽  
SETH COPEN GOLDSTEIN ◽  
FRANK PFENNING
Keyword(s):  
Data Structure ◽  
Logic Programming ◽  
Programming Languages ◽  
Programming Language ◽  
Linear Logic ◽  
Operational Semantics ◽  
Concurrent Programming ◽  
Logical System ◽  
Logic Programming Language ◽  
Graph Data

AbstractWe have designed a new logic programming language called LM (Linear Meld) for programming graph-based algorithms in a declarative fashion. Our language is based on linear logic, an expressive logical system where logical facts can be consumed. Because LM integrates both classical and linear logic, LM tends to be more expressive than other logic programming languages. LM programs are naturally concurrent because facts are partitioned by nodes of a graph data structure. Computation is performed at the node level while communication happens between connected nodes. In this paper, we present the syntax and operational semantics of our language and illustrate its use through a number of examples.

scholarly journals Batched evaluation of linear tabled logic programs

2013 ◽  
Vol 10 (4) ◽  
pp. 1775-1797
Author(s):  
Miguel Areias ◽  
Ricardo Rocha
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Execution Time ◽  
Scheduling Algorithm ◽  
Logic Programs ◽  
Resolution Limit ◽  
Powerful Technique ◽  
Programming Paradigm ◽  
Sld Resolution ◽  
Local Scheduling

Logic Programming languages, such as Prolog, provide a highlevel, declarative approach to programming. Despite the power, flexibility and good performance that Prolog systems have achieved, some deficiencies in Prolog?s evaluation strategy - SLD resolution - limit the potential of the logic programming paradigm. Tabled evaluation is a recognized and powerful technique that overcomes SLD?s susceptibility in dealing with recursion and redundant sub-computations. In a tabled evaluation, there are several points where we may have to choose between different tabling operations. The decision on which operation to perform is determined by the scheduling algorithm. The two most successful tabling scheduling algorithms are local scheduling and batched scheduling. In previous work, we have developed a framework, on top of the Yap Prolog system, that supports the combination of different linear tabling strategies for local scheduling. In this work, we propose the extension of our framework to support batched scheduling. In particular, we are interested in the two most successful linear tabling strategies, the DRA and DRE strategies. To the best of our knowledge, no other Prolog system supports both strategies simultaneously for batched scheduling. Our experimental results show that the combination of the DRA and DRE strategies can effectively reduce the execution time for batched evaluation.

Sign in / Sign up

Export Citation Format

Share Document