检索结果-内蒙古大学图书馆

The Computational Relevance of Formal logic Through Formal Proofs 3rd

The Computational Relevance of Formal Logic Through Formal P...

3rd international Formal Methods Teaching workshop (FMTea) Held as Part of the 3rd World Congress on Formal Methods (FM)

作者： Almeida, Ariane A. Rocha-Oliveira, Ana Cristina Ferreira Ramos, Thiago M. de Moura, Flavio L. C. Ayala-Rincon, Mauricio Univ Brasilia Dept Ciencia Comp BR-70910900 Brasilia DF Brazil Univ Brasilia Dept Matemat BR-70910900 Brasilia DF Brazil

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.

关键词： Formal logic

来源：评论

学校读者我要写书评

暂无评论

A preliminary report on integrating of answer set and constraint solving

A preliminary report on integrating of answer set and constr...

引用

3rd international workshop on Answer Set programming: Advances in Theory and Implementation, ASP 2005, Co-located Event with the 19th international Joint Conference on Artificial Intelligence, IJCAI 2005

作者： Baselice, Sabrina Bonatti, Piero Gelfond, M. Dipartimento di Scienze Fisiche Università Federico II Complesso Universitario di Monte Sant'Angelo Via Cinthia Napoli Italy Texas Tech. University Department of Computer Science Lubbock TX United States

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.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Software Engineering and Formal Methods 1

引用

丛书名： Lecture Notes in Computer Science

1000年

作者： Carlos Canal Akram Idani

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 3rd international Symposium on Modelling and knowledge Management Applications - Systems and Domains, MoKMaSD 2014, the 8th international workshop 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.

关键词： logics and Meanings of Programs Software Engineering programming Languages, Compilers, Interpreters Mathematical logic and Formal Languages

来源：评论

学校读者我要写书评

暂无评论

CEUR workshop Proceedings

CEUR Workshop Proceedings

引用

3rd international workshop on Sets and Tools, SETS 2018

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 in equilibrium logic and answer set programming: The propositional case 3

Interpolation in equilibrium logic and answer set programmin...

引用

3rd workshop on Answer Set programming and Other Computing Paradigms, ASPOCP 2010 - Collocated with the international Conference on logic programming, ICLP 2010

作者： Gabbay, Dov Pearce, David Valverde, Agustín King's College London United Kingdom AI Dept Universidad Politécnica de Madrid Spain Dept of Applied Mathematics Universidad de Málaga Spain

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 propositional version of the non-monotonic system of equilibrium logic, establishing weaker or stronger forms of interpolation depending on the precise interpretation of the inference relation. These results also yield a form of interpolation for ground logic programs under the answer sets semantics. For disjunctive logic programs we also study the property of uniform interpolation that is closely related to the concept of variable forgetting. © 2020 workshop on Answer Set programming and Other Computing Paradigms, ASPOCP 2010. All rights reserved.

关键词： Interpolation

来源：评论

学校读者我要写书评

暂无评论

Proposal of a High-Level Language for Writing Self Modifying Programs

引用

IEEE LATIN AMERICA TRANSACTIONS 2011年第2期9卷 192-198页

作者： da Silva, S. R. B. Neto, J. J. Univ Estado Amazonas Curso Engn Computacao Manaus Amazonas Brazil Univ Sao Paulo Escola Politecn Sao Paulo Brazil

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.

关键词： Adaptivity programming language self modifying code adaptive technology

来源：评论

学校读者我要写书评

暂无评论

Diverse Applications of an Automated Argument System Based on the logic of Multiple-Valued Argumentation

Diverse Applications of an Automated Argument System Based o...

引用

8th Pacific Rim international workshop on Multi-Agents (PRIMA 2005)

作者： Jeong, Gowun Sawamura, Hajime Korea Adv Inst Sci & Technol Dept Comp Sci Taejon 305701 South Korea Niigata Univ Inst Natl Sci &Technol Acad Assembly Niigata Japan

ISBN: (纸本)9783642033377

A logic of Multiple-valued Argumentation (LMA) was formalized by Takahashi and Sawamura on an expressive knowledge representation language, Extended Annotated logic programming (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.

关键词： Decision making

来源：评论

学校读者我要写书评

暂无评论

A logic-based approach to system modelling 91

A logic-based approach to system modelling

引用

3rd international workshop on Software Configuration Management, SCM 1991

作者： Rich, Anthony Solomon, Marvin University of Wisconsin-Madison United States Computer Sciences Department 1210 W. Dayton St. MadisonWI53706 United States

ISBN: (纸本)0897914295

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 logic programming. A declarative system model is developed in which objects are expressed as terms that describe their form, functionality, composition, and origin. For example, the form of a Pascal compiler written in C is "C";its functionality is to translate an object whose form is "Pascal" into an object of form "object code" while preserving functionality. Terms are patterns that can be matched against those of other object descriptions and tool signatures using unification. Derived objects are requested by specifying a goal object having the desired form and functionality. A planning algorithm finds derivation paths in the system model from source objects to the goal. The planner produces a build plan—a logic program that, when executed, can produce the goal using the software development tools in the environment. All aspects of a software configuration are specified in a single language. Large software specifications can be described in discrete, manageable pieces. We present our approach in detail by working through an extended example. We discuss its advantages and limitations and outline our plans for further research on its applicability to a variety of problems in system specification and building. © 1991 ACM.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Agent-oriented programming with underlying ontological reasoning

Agent-oriented programming with underlying ontological reaso...

引用

3rd international workshop on Declarative Agent Languages and Technologies, DALT 2005

作者： Moreira, Álvaro F. Vieira, Renata Bordini, Rafael H. Hübner, Jomi F. Universidade Federal do Rio Grande do Sul Brazil Universidade do Vale do Rio dos Sinos Brazil University of Durham United Kingdom Universidade Regional de Blumenau Brazil

ISBN: (纸本)3540331069

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 trends in computer science such as grid-based and ubiquitous computing. In this paper, we formally define a version of the BDI agent-oriented programming language AgentSpeak based on description logic rather than predicate logic. In this approach, the belief base of an agent contains the definition of complex concepts, besides specific factual knowledge. We illustrate the approach using examples based on the wellknown smart meeting-room scenario. The advantages of combining AgentSpeak with description logics are: (i) queries to the belief base are more expressive as their results do not rely only on explicit knowledge but can be inferred from the ontology;(ii) the notion of belief update is refined given that (ontological) consistency of a belief addition can be checked;(iii) retrieving a plan for handling an event is more flexible as it is not based solely on unification but on the subsumption relation between concepts;and (iv) agents may share knowledge by using ontology languages such as OWL. Extending agent programming languages with description logics can have a significant impact on the development of multiagent systems for the semantic web. © Springer-Verlag Berlin Heidelberg 2006.

关键词： Computer programming

来源：评论

学校读者我要写书评

暂无评论

An Evaluative Model to Assess the Organizational Efficiency in Training Corporations 3rd

引用

3rd international Conference on Future Data and Security Engineering (FDSE) / 10th international Conference on Advanced Computing and Applications (ACOMP)

作者： Fernandes, Ana Vicente, Henrique Figueiredo, Margarida Neves, Mariana Neves, Jose Org Multinacl Formacao Lisbon Portugal Univ Evora Dept Quim Escola Ciencias & Tecnol Evora Portugal Univ Minho Ctr Algoritmi Braga Portugal Univ Evora Ctr Invest Educ & Psicol Evora Portugal Deloitte London England

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 logic programming 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.

关键词： Optimization Efficiency logic programming knowledge representation Artificial neural networks

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：