Environments for systematic construction of logic programs are needed in the academy as well as in the industry. Such environments should support well defined construction methods and should be able to be extended and interact with other programming tools like debuggers and compilers. We present a variant of the Deville methodology for logic program development, and the design of a tool for supporting the methodology. Our aim is to facilitate the learning of logic programming and to set the basis of more sophisticated tools for program development.
Logic programming is a flexible programming paradigm due to the use of predicates without a fixed data flow. To extend logic languages with the compact notation of functional programming, there are various proposals to map evaluable functions into predicates in order to stay in the logic programming framework. Since amalgamated functional logic languages offer flexible as well as efficient evaluation strategies, we propose an opposite approach in this paper. By mapping logic programs into functional logic programs with a transformation based on inferring functional dependencies, we develop a f…
Logic program transformation by the unfold/fold method ad- vocates the writing of correct logic programs via the application of some rules to a naive program. This work focuses on how to overcome subgoal- introduction difficulties in synthesizing efficient sorting algorithms from an naive sorting algorithm, through logic program transformation and abductive reasoning.
Constraint-logic object-oriented programming provides a useful symbiosis between object-oriented programming and constraint-logic search. The ability to use logic variables, constraints, non-deterministic search, and object-oriented programming in an integrated way facilitates the combination of search-related program parts and other business logic in object-oriented applications. With this work we conceptualize array-typed logic variables ("free arrays"), thus completing the set of types that logic variables can assume in constraint-logic object-oriented programming. Free arrays exhibit inter…
Constraint-logic object-oriented programming, for example using Muli, facilitates the integrated development of business software that occasionally involves finding solutions to constraint-logic problems. The availability of object-oriented features calls for the option to use objects as logic variables as well, as opposed to being limited to primitive type logic variables. The present work contributes a concept for reference type logic variables in constraint-logic object-oriented programming that takes arbitrary class hierarchies of programs written in object-oriented languages into account.…
The Workshops on (Constraint) Logic Programming (WLP) are the annual meeting of the German Society of Logic Programming (Gesellschaft für Logische Programmierung e.V., GLP) and bring together researchers interested in logic programming, constraint programming, answer set programming, and related areas like databases and artificial intelligence (not only from Germany). The International Workshops on Functional and (Constraint) Logic Programming (WFLP) aim at bringing together researchers, students, and practitioners interested in functional programming, logic programming, and their integration.…
A Proof Theoretic Approach to Failure in Functional Logic Programming
如何从程序中提取负信息是逻辑程序设计中的一个重要问题。在这里，我们解决问题的功能逻辑程序，从证明理论的角度来看。我们工作的出发点是CRWL（Constructor based ReWriting Logic），它是一个成熟的函数逻辑编程理论框架，其基本概念是非严格非确定函数。我们提出了一个证明演算，CRWLF，这是能够推导出否定信息的CRWL程序。特别是，CRWLF能够证明CRWL内的复位有限失败。
This volume constitutes the pre-proceedings of the 28th International Workshop on Functional and Logic Programming (WFLP 2020), organized by the University of Bologna, Italy, as part of Bologna Federated Conference on Programming Languages 2020. The international Workshop on Functional and (constraint) Logic Programming (WFLP) aims at bringing together researchers, students, and practitioners interested in functional programming, logic programming, and their integration. WFLP has a reputation for being a lively and friendly forum, and it is open for presenting and discussing work in progress, …
Logic programming such as Prolog is often sequential and slow because each execution step processes only a single, $micro$ connective. To fix this problem, we propose to use $macro$ connectives as the means of improving both readability and performance.
We present an experimental system strongly inspired by miniKanren, implemented on top of the tactics mechanism of the HOL~Light theorem prover. Our tool is at the same time a mechanism for enabling the logic programming style for reasoning and computing in a theorem prover, and a framework for writing logic programs that produce solutions endowed with a formal proof of correctness.
The semantic foundations for logic programming are usually separated into two different approaches. The operational semantics, which uses SLD-resolution, the proof method that computes answers in logic programming, and the declarative semantics, which sees logic programs as formulas and its semantics as models. Here, we define a new operational semantics called TSLD-resolution, which stands for Typed SLD-resolution, where we include a value "wrong", that corresponds to the detection of a type error at run-time. For this we define a new typed unification algorithm. Finally we prove the correctn…
Formal verification provides strong guarantees of correctness of software, which are especially important in safety or security critical systems. Hoare logic is a widely used formalism for rigorous verification of software against specifications in the form of pre-condition/post-condition assertions. The advancement of semantic parsing techniques and higher computational capabilities enable us to extract semantic content from natural language text as formal logical forms, with increasing accuracy and coverage. This paper proposes a formal framework for Hoare logic-based formal verification of …
Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this paper, we will survey the use of structural proof theory as an alternative foundation. Researchers have been using this foundation for the past 35 years to elevate logic programming from its roots in first-order classical logic into higher-order versions of intuitionistic and linear logic. These more expressive logic programming languages allow for capturing stateful computations and rich forms of abstractions, including higher-order programming, modularity, and abstract d…
The Workshop on Coalgebra, Horn Clause Logic Programming and Types was held on the 28-29 November 2016 in Edinburgh. The workshop marked the end of the EPSRC Grant Coalgebraic Logic Programming for Type Inference, by E. Komendantskaya, Heriot-Watt University and J. Power, University of Bath, UK.
{\em Computability logic} (CoL) is a powerful computational model which views computational problems as games played by a machine and its environment. In this paper, we show that CoL naturally supports multiagent programming models with distributed control. To be specific, we discuss a distributed logic programming model based on CoL (CL1 to be exact), which we call CL1^Ω. The key feature of this model is that it supports $dynamic/evolving$ knowledgebase of an agent. This model turns out to be a promising approach to reaching both general AI and future computing model.
We extend a technique called Compiling Control. The technique transforms coroutining logic programs into logic programs that, when executed under the standard left-to-right selection rule (and not using any delay features) have the same computational behavior as the coroutining program. In recent work, we revised Compiling Control and reformulated it as an instance of Abstract Conjunctive Partial Deduction. This work was mostly focused on the program analysis performed in Compiling Control. In the current paper, we focus on the synthesis of the transformed program. Instead of synthesizing a ne…
Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Contributions are sought in all areas of logic programming, including but not restricted to: Foundations: Semantics, Formalisms, Nonmonotonic reasoning, Knowledge representation. Languages: Concurrency, Objects, Coordination, Mobility, Higher Order, Types, Modes, Assertions, Modules, Meta-programming, Logic-based domain-specific languages, Programming Techniques. Declarative programming: Declarative program development, Analysis, Type and mode infere…
Fuzzy logic programming is a growing declarative paradigm aiming to integrate fuzzy logic into logic programming. One of the most difficult tasks when specifying a fuzzy logic program is determining the right weights for each rule, as well as the most appropriate fuzzy connectives and operators. In this paper, we introduce a symbolic extension of fuzzy logic programs in which some of these parameters can be left unknown, so that the user can easily see the impact of their possible values. Furthermore, given a number of test cases, the most appropriate values for these parameters can be automat…
We survey the landscape of Hoare logics for quantum programs. We review three papers: "Reasoning about imperative quantum programs" by Chadha, Mateus and Sernadas; "A logic for formal verification of quantum programs" by Yoshihiko Kakutani; and "Floyd-hoare logic for quantum programs" by Mingsheng Ying. We compare the mathematical foundations of the logics, their underlying languages, and the expressivity of their assertions. We also use the languages to verify the Deutsch-Jozsa Algorithm, and discuss their relative usability in practice.
Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Contributions are solicited in all areas of logic programming and related areas, including but not restricted to: - Foundations: Semantics, Formalisms, Answer-Set Programming, Non-monotonic Reasoning, Knowledge Representation. - Declarative Programming: Inference engines, Analysis, Type and mode inference, Partial evaluation, Abstract interpretation, Transformation, Validation, Verification, Debugging, Profiling, Testing, Logic-based domain-specific …
Higher-order logic programming is an interesting extension of traditional logic programming that allows predicates to appear as arguments and variables to be used where predicates typically occur. Higher-order characteristics are indeed desirable but on the other hand they are also usually more expensive to support. In this paper we propose a program specialization technique based on partial evaluation that can be applied to a modest but useful class of higher-order logic programs and can transform them into first-order programs without introducing additional data structures. The resulting fir…
This paper presents an example of formal reasoning about the semantics of a Prolog program of practical importance (the SAT solver of Howe and King). The program is treated as a definite clause logic program with added control. The logic program is constructed by means of stepwise refinement, hand in hand with its correctness and completeness proofs. The proofs are declarative - they do not refer to any operational semantics. Each step of the logic program construction follows a systematic approach to constructing programs which are provably correct and complete. We also prove that correctness…
We present VAEL, a neuro-symbolic generative model integrating variational autoencoders (VAE) with the reasoning capabilities of probabilistic logic (L) programming. Besides standard latent subsymbolic variables, our model exploits a probabilistic logic program to define a further structured representation, which is used for logical reasoning. The entire process is end-to-end differentiable. Once trained, VAEL can solve new unseen generation tasks by (i) leveraging the previously acquired knowledge encoded in the neural component and (ii) exploiting new logical programs on the structured laten…
This volume constitutes the pre-proceedings of the 26th International Workshop on Functional and Logic Programming (WFLP 2018). It is formed of those papers selected by the program committee for presentation at the workshop. After discussion at the workshop, the program committee will select a number of papers to be invited for the second round of refereeing and selection for the formal proceedings.
This volume constitutes the informal proceedings of the 32nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2022), held on 21-23rd September 2022 as a hybrid (blended) meeting, both in-person (at the Ivane Javakhishvili Tbilisi State University -TSU- in Tbilisi, Georgia) and virtual, and co-located with the 24th International Symposium on Principles and Practice of Declarative Programming (PPDP 2022) as part of the Computational Logic Autumn Summit 2022 (CLAS 2022).
Research on deductive verification of probabilistic programs has considered expectation-based logics, where pre- and post-conditions are real-valued functions on states, and assertion-based logics, where pre- and post-conditions are boolean predicates on state distributions. Both approaches have developed over nearly four decades, but they have different standings today. Expectation-based systems have managed to formalize many sophisticated case studies, while assertion-based systems today have more limited expressivity and have targeted simpler examples. We present Ellora, a sound and relativ…
We present a program logic for Pitts and Stark's ν-calculus, an extension of the call-by-value simply-typed λ-calculus with a mechanism for the generation of fresh names. Names can be compared for (in)-equality, producing programs with subtle observable properties. Hidden names produced by interactions between generation and abstraction are captured logically with a second-order quantifier over type contexts. We illustrate usage of the logic through reasoning about well-known difficult cases from the literature.
