We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is cast in terms of coinductive ...
详细信息
ISBN:
(纸本)9783030171841;9783030171834
We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is cast in terms of coinductive uniform proofs;its constructive content is exposed via soundness relative to an intuitionistic first-order logic with recursion controlled by the later modality;and soundness of both proof systems is proven relative to a novel coalgebraic description of complete Herbrand models.
We present a logical framework allowing us to express assessment of facts (is it proven?) and arguments (is it sound?) together with a proof system to answer these questions. Our motivation is to clarify the notion of...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
We present a logical framework allowing us to express assessment of facts (is it proven?) and arguments (is it sound?) together with a proof system to answer these questions. Our motivation is to clarify the notion of validity in the context of logic-based arguments along different aspects (such as the formulas used and the inference scheme). Originality lies in the possibility for the user to design their own argument schemes. We show that classical inference obtains when arguments are based on classical schemes (e.g. Hilbert axioms). We go beyond classical logic by distinguishing "proven" formulas from "uncontroversial" ones (whose negation is not proven). Hence a formal definition of a fallacious argument: it uses controversial formulas or schemes recognized as illicit. We express some rational arguments and fallacies in the form of schemes.
Combining theory and practice, Website Design and Development with HTML5 and CSS3 is aimed at both beginners who want to design their first website, and experienced developers who want to consolidate their technical s...
详细信息
ISBN:
(数字)9781119885122
ISBN:
(纸本)9781786306968
Combining theory and practice, Website Design and Development with HTML5 and CSS3 is aimed at both beginners who want to design their first website, and experienced developers who want to consolidate their technical skills. This book addresses the theoretical aspects of HTML5 and CSS3, including: HTML elements, semantic containers, semantic text formatting, multimedia elements, forms, tables, definition and integration of CSS styles, text formatting, and container and box styles. It also encompasses a practical section which presents the process of creating a website, as well as the key rules to apply in order to not only achieve project success, but also to meet user needs. Illustrated by numerous examples, this book includes corrected practical work, structured according to an evolutionary logic ranging from the design of a simple HTML5 page to the creation of a professional website.
We focus on the problem of inducing logic programs that explain models learned by the support vector machine (SVM) algorithm. The top-down sequential covering inductive logicprogramming (ILP) algorithms (e.g., FOIL) ...
详细信息
We extend probabilistic action language pBC+ with the notion of utility in decision theory. The semantics of the extended pBC+ can be defined as a shorthand notation for a decision-theoretic extension of the probabili...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
We extend probabilistic action language pBC+ with the notion of utility in decision theory. The semantics of the extended pBC+ can be defined as a shorthand notation for a decision-theoretic extension of the probabilistic answer set programming language LPMLN. Alternatively, the semantics of pBC+ can also be defined in terms of Markov Decision Process (MDP), which in turn allows for representing MDP in a succinct and elaboration tolerant way as well as leveraging an MDP solver to compute a pBC+ action description. The idea led to the design of the system PBCPLUS2MDP, which can find an optimal policy of a pBC+ action description using an MDP solver.
This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a ...
详细信息
We present the design of a new functional programming language, MLTS, that uses the lambda-tree syntax approach to encoding bindings appearing within data structures. In this approach, bindings never become free nor e...
详细信息
ISBN:
(纸本)9781450372497
We present the design of a new functional programming language, MLTS, that uses the lambda-tree syntax approach to encoding bindings appearing within data structures. In this approach, bindings never become free nor escape their scope: instead, binders in data structures are permitted to move to binders within programs. The design of MLTS includes additional sites within programs that directly support this movement of bindings. In order to formally define the language's operational semantics, we present an abstract syntax for MLTS and a natural semantics for its evaluation. We shall view such natural semantics as a logical theory within a rich logic that includes both nominal abstraction and the del-quantifier: as a result, the natural semantics specification of MLTS can be given a succinct and elegant presentation. We present a typing discipline that naturally extends the typing of core ML programs and we illustrate the features of MLTS by presenting several examples. An on-line interpreter for MLTS is briefly described.
Computer scientists are well-versed in dealing with data structures. The same cannot be said about their dual: codata. Even though codata is pervasive in category theory, universal algebra, and logic, the use of codat...
详细信息
ISBN:
(纸本)9783030171841;9783030171834
Computer scientists are well-versed in dealing with data structures. The same cannot be said about their dual: codata. Even though codata is pervasive in category theory, universal algebra, and logic, the use of codata for programming has been mainly relegated to representing infinite objects and processes. Our goal is to demonstrate the benefits of codata as a general-purpose programming abstraction independent of any specific language: eager or lazy, statically or dynamically typed, and functional or object-oriented. While codata is not featured in many programming languages today, we show how codata can be easily adopted and implemented by offering simple inter-compilation techniques between data and codata. We believe codata is a common ground between the functional and object-oriented paradigms;ultimately, we hope to utilize the Curry-Howard isomorphism to further bridge the gap.
Adding predicate subtyping to higher-order logic yields a very expressive language in which type-checking is undecidable, making the definition of a system of verifiable certificates challenging. This work presents a ...
详细信息
ISBN:
(纸本)9783030171841;9783030171834
Adding predicate subtyping to higher-order logic yields a very expressive language in which type-checking is undecidable, making the definition of a system of verifiable certificates challenging. This work presents a solution to this issue with a minimal formalization of predicate subtyping, named PVS-Core, together with a system of verifiable certificates for PVS-Core, named PVS-Cert. PVS-Cert is based on the introduction of proof terms and explicit coercions. Its design is similar to that of PTSs with dependent pairs, with the exception of the definition of conversion, which is based on a specific notion of reduction -> (beta*), corresponding to beta-reduction combined with the erasure of coercions. The use of this reduction instead of the more standard reduction -> (beta sigma) allows to establish a simple correspondence between PVS-Core and PVS-Cert. On the other hand, a type-checking algorithm is designed for PVS-Cert, built on proofs of type preservation of -> (beta sigma) and strong normalization of both -> (beta sigma) and -> (beta*). Combining these results, PVS-Cert judgements are used as verifiable certificates for predicate subtyping. In addition, the reduction -> (beta sigma) is used to define a cut elimination procedure for predicate subtyping. This definition provides a new tool to study the properties of predicate subtyping, as illustrated with a proof of consistency.
Answer set programming (ASP) is a programming methodology oriented towards combinatorial search problems. In such a problem, the goal is to find a solution among a large but finite number of possibilities. The idea of...
ISBN:
(数字)9783030246587
ISBN:
(纸本)9783030246570
Answer set programming (ASP) is a programming methodology oriented towards combinatorial search problems. In such a problem, the goal is to find a solution among a large but finite number of possibilities. The idea of ASP came from research on artificial intelligence and computational logic. ASP is a form of declarative programming: an ASP program describes what is counted as a solution to the problem, but does not specify an algorithm for solving it. Search is performed by sophisticated software systems called answer set solvers. Combinatorial search problems often arise in science and technology, and ASP has found applications in diverse areas―in historical linguistic, in bioinformatics, in robotics, in space exploration, in oil and gas industry, and many others. The importance of this programming method was recognized by the Association for the Advancement of Artificial Intelligence in 2016, when AI Magazine published a special issue on answer set programming. The book will introduce the reader to the theory and practice of ASP. It will describe the input language of the answer set solver CLINGO, which was designed at the University of Potsdam in Germany and is used today by ASP programmers in many countries. It will include numerous examples of ASP programs and present the mathematical theory that ASP is based on. There will be many exercises with complete solutions.
暂无评论