The construction of correct software, i.e. a computer program that meets a given specification, is an important goal in Computer Science. Nowadays, not only critical software (the ones used in aircraft, hospitals, ban...
详细信息
ISBN:
(纸本)9783030324414;9783030324407
The construction of correct software, i.e. a computer program that meets a given specification, is an important goal in Computer Science. Nowadays, not only critical software (the ones used in aircraft, hospitals, banks, etc.) is supposed to provide additional guarantees of its correctness. Nevertheless, this is not an easy task because proofs are often long and full of details. In this sense, a strong background in logical deduction is essential to provide Computer Science (CS) professionals the necessary competencies to understand and provide mathematical proofs of their programs. logic courses for CS tend to follow old precepts without emphasizing mastering deduction itself. In our institution, for several years we have followed a more pragmatical approach, in which the foundational aspects of both natural deduction and deduction a la Gentzen are taught and, in parallel, the operational premises of deduction are put into practice in proof assistants. Thus, CS students with a minimum knowledge in programming are challenged on providing correctness certificates for simple algorithms. "Putting their hands in the dough" they acquire a better understanding of the value and importance of deductive technologies in computing. Here we show how this is done relating natural deduction and sequent calculus deduction and using the proof assistant PVS in the simple context of a library of sorting algorithms.
Despite all efforts on intelligent grounding, state-of-the-art answer set solvers still have huge memory requirements, because they compute the ground instantiation of the input program before the actual reasoning sta...
详细信息
Despite all efforts on intelligent grounding, state-of-the-art answer set solvers still have huge memory requirements, because they compute the ground instantiation of the input program before the actual reasoning starts. This prevents ASP to be effective on several classes of problems. In this paper we integrate answer set generation and constraint solving to reduce the memory requirements for a class of multi-sorted logic programs with cardinality constraints. We prove some theoretical results, introduce a provably sound and complete algorithm, and report experimental results showing that our approach can solve problem instances with significantly larger domains.
This book constitutes revised selected papers from the workshops collocated with the SEFM 2014 conference on Software Engineering and Formal Methods, held in Grenoble, France, in September 2014. The 26 papers included...
详细信息
ISBN:
(数字)9783319152011
ISBN:
(纸本)9783319152004
This book constitutes revised selected papers from the workshops collocated with the SEFM 2014 conference on Software Engineering and Formal Methods, held in Grenoble, France, in September 2014. The 26 papers included in this volume were carefully reviewed and selected from 49 submissions. They are from the following workshops: the 1st workshop on Human-Oriented Formal Methods - From Readability to Automation, HOFM 2014, the 3rdinternational Symposium on Modelling and knowledge Management Applications - Systems and Domains, MoKMaSD 2014, the 8th internationalworkshop on Foundations and Techniques for Open Source Software Certification, Open Cert 2014, the 1st workshop on Safety and Formal Methods, SaFoMe 2014 and the 4th workshop on Formal Methods in the Development of Software, WS-FMDS 2014.
The proceedings contain 6 papers. The topics discussed include: solving set constraints in B and event-B: foundations and applications;encoding sets as real numbers;programming in Java with restricted intensional sets...
The proceedings contain 6 papers. The topics discussed include: solving set constraints in B and event-B: foundations and applications;encoding sets as real numbers;programming in Java with restricted intensional sets;towards Coq formalisation of {log} set constraints resolution;on perfect matchings for some bipartite graphs;a set-based reasoner for the description logic DL4,x D;and polarized rewriting and tableaux in B set theory.
Interpolation is an important property of classical and many non classical logics that has been shown to have interesting applications in computer science and AI. Here we study the Interpolation Property for the propo...
详细信息
This paper proposes a simple high-level programming language, endowed with resources that help encoding self-modifying programs. With this purpose, a conventional imperative language syntax (not explicitly stated in t...
详细信息
This paper proposes a simple high-level programming language, endowed with resources that help encoding self-modifying programs. With this purpose, a conventional imperative language syntax (not explicitly stated in this paper) is incremented with special commands and statements forming an adaptive layer specially designed with focus on the dynamical changes to be applied to the code at run-time. The resulting language allows programmers to easily specify dynamic changes to their own program's code. Such a language succeeds to allow programmers to effortless describe the dynamic logic of their adaptive applications. In this paper, we describe the most important aspects of the design and implementation of such a language. A small example is finally presented for illustration purposes.
A logic of Multiple-valued Argumentation (LMA) was formalized by Takahashi and Sawamura on an expressive knowledgerepresentation language, Extended Annotated logicprogramming (EALP). LMA allows agents to construct a...
详细信息
ISBN:
(纸本)9783642033377
A logic of Multiple-valued Argumentation (LMA) was formalized by Takahashi and Sawamura on an expressive knowledgerepresentation language, Extended Annotated logicprogramming (EALP). LMA allows agents to construct arguments under uncertain knowledge and to argue with other agents on uncertain issues in the open networked heterogeneous environment. In this paper, we demonstrate its expressiveness and applicability through implementing it in a networked environment and applying it to diverse uncertain domains in which decision-making is sought in an argumentative way. We then show that it is the diversity of truth values in LMA that allows for an extensive applicability of it.
Modelling a complex software system requires a description of how its components are related to one another. We propose a new approach to this problem based on logicprogramming. A declarative system model is develope...
详细信息
Developing applications that make effective use of machine-readable knowledge sources as promised by the Semantic Web vision is attracting much of current research interest;this vision is also affecting important tren...
详细信息
In an organisation any optimization process of its issues faces increasing challenges and requires new approaches to the organizational phenomenon. Indeed, in this work it is addressed the problematic of efficiency dy...
详细信息
ISBN:
(纸本)9783319480572;9783319480565
In an organisation any optimization process of its issues faces increasing challenges and requires new approaches to the organizational phenomenon. Indeed, in this work it is addressed the problematic of efficiency dynamics through intangible variables that may support a different view of the corporations. It focuses on the challenges that information management and the incorporation of context brings to competitiveness. Thus, in this work it is presented the analysis and development of an intelligent decision support system in terms of a formal agenda built on a logicprogramming based methodology to problem solving, complemented with an attitude to computing grounded on Artificial Neural Networks. The proposed model is in itself fairly precise, with an overall accuracy, sensitivity and specificity with values higher than 90 %. The proposed solution is indeed unique, catering for the explicit treatment of incomplete, unknown, or even self-contradictory information, either in a quantitative or qualitative arrangement.
暂无评论