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

A Classical Sequent Calculus with Dependent Types 26th

A Classical Sequent Calculus with Dependent Types

26th European Symposium on programming (ESOP) Held as Part of the European Joint Conferences on theory and practice of Software (ETAPS)

作者： Miquey, Etienne Univ Paris Diderot IRIF PI R2 INRIA Paris France Univ Republica Fac Ingn IMERL Montevideo Uruguay

ISBN: (纸本)9783662544341;9783662544334

Dependent types are a key feature of type systems, typically used in the context of both richly-typed programming languages and proof assistants. Control operators, which are connected with classical logic along the proof-as-program correspondence, are known to misbehave in the presence of dependent types, unless dependencies are restricted to values. We place ourselves in the context of the sequent calculus which has the ability to smoothly provide control under the form of the mu operator dual to the common let operator, as well as to smoothly support abstract machine and continuation-passing style interpretations. We start from the call-by-value version of the lambda mu(mu) over tilde language and design a minimal language with a value restriction and a type system that includes a list of explicit dependencies and maintains type safety. We then show how to relax the value restriction and introduce delimited continuations to directly prove the consistency by means of a continuation-passing-style translation. Finally, we relate our calculus to a similar system by Lepigre [19], and present a methodology to transfer properties from this system to our own.

关键词： Dependent types Sequent calculus Classical logic Control operators Call-by-value Delimited continuations Continuation-passing style translation Value restriction

来源：评论

学校读者我要写书评

暂无评论

Constraint programming for Multi-criteria Conceptual Clustering 23rd

Constraint Programming for Multi-criteria Conceptual Cluster...

引用

33rd International Conference on logic programming / 23rd International Conference on Principles and practice of Constraint programming (CP) / 20th International Conference on theory and Applications of Satisfiability Testing (SAT)

作者： Chabert, Maxime Solnon, Christine Univ Lyon INSA Lyon LIRIS F-69622 Villeurbanne France Infologic Bourg Les Valence France

ISBN: (纸本)9783319661582;9783319661575

A conceptual clustering is a set of formal concepts (i.e., closed itemsets) that defines a partition of a set of transactions. Finding a conceptual clustering is an NP-complete problem for which Constraint programming (CP) and Integer Linear programming (ILP) approaches have been recently proposed. We introduce new CP models to solve this problem: a pure CP model that uses set constraints, and an hybrid model that uses a data mining tool to extract formal concepts in a preprocessing step and then uses CP to select a subset of formal concepts that defines a partition. We compare our new models with recent CP and ILP approaches on classical machine learning instances. We also introduce a new set of instances coming from a real application case, which aims at extracting setting concepts from an Enterprise Resource Planning (ERP) software. We consider two classic criteria to optimize, i.e., the frequency and the size. We show that these criteria lead to extreme solutions with either very few small formal concepts or many large formal concepts, and that compromise clusterings may be obtained by computing the Pareto front of non dominated clusterings.

关键词： Constraint programming

来源：评论

学校读者我要写书评

暂无评论

ArgueApply: A Mobile App for Argumentation 14th

ArgueApply: A Mobile App for Argumentation

引用

14th International Conference on logic programming and Nonmonotonic Reasoning (LPNMR)

作者： Puehrer, Joerg Univ Leipzig Inst Comp Sci Leipzig Germany

ISBN: (纸本)9783319616605;9783319616599

Formal models developed in the field of argumentation allow for analysing and evaluating problems that have previously been studied by philosophers on an informal level only. Importantly, they also give rise to the development of computational tools for argumentation. In this paper we report on ArgueApply, a mobile app for argumentation that is based on the Grappa framework, an extension of, e.g., abstract argumentation in the sense of Dung. With ArgueApply users can engage in online discussions and evaluate their semantics. Each of the resulting interpretations can be seen as a coherent view on a discussion in which some of the discussions statements are accepted and others rejected. Being a mobile tool, ArgueApply is intended to be more accessible than existing systems for computing argumentation semantics allowing, e.g., for spontaneous analysis of an ongoing discussion or collective preparation for an important debate. While having a practical system for these applications is the final goal of our work, an immediate objective is using the system for exploring which type of Grappa frameworks under which semantics are best suited for such applications.

关键词： Argumentation Grappa Mobile application Android Answer-set programming

来源：评论

学校读者我要写书评

暂无评论

Reduced Cost Fixing in MaxSAT 23rd

Reduced Cost Fixing in MaxSAT

引用

作者： Bacchus, Fahiem Hyttinen, Antti Jarvisalo, Matti Saikko, Paul Univ Toronto Dept Comp Sci Toronto ON Canada Univ Helsinki HIIT Dept Comp Sci Helsinki Finland

ISBN: (纸本)9783319661582;9783319661575

We investigate utilizing the integer programming (IP) technique of reduced cost fixing to improve maximum satisfiability (MaxSAT) solving. In particular, we show how reduced cost fixing can be used within the implicit hitting set approach (IHS) for solving MaxSAT. Solvers based on IHS have proved to be quite effective for MaxSAT, especially on problems with a variety of clause weights. The unique feature of IHS solvers is that they utilize both SAT and IP techniques. We show how reduced cost fixing can be used in this framework to conclude that some soft clauses can be left falsified or forced to be satisfied without influencing the optimal cost. Applying these forcings simplifies the remaining problem. We provide an extensive empirical study showing that reduced cost fixing employed in this manner can be useful in improving the state-of-the-art in MaxSAT solving especially on hard instances arising from real-world application domains.

关键词： Integer programming

来源：评论

学校读者我要写书评

暂无评论

Symmetric Explanation Learning: Effective Dynamic Symmetry Handling for SAT 1

引用

33rd International Conference on logic programming colocated with the 23rd International Conference on Principles and practice of Constraint programming / 20th International Conference on theory and Applications of Satisfiability Testing

作者： Devriendt, Jo Bogaerts, Bart Bruynooghe, Maurice Katholieke Univ Leuven Dept Comp Sci Celestijnenlaan 200A B-3001 Heverlee Belgium

ISBN: (数字)9783319662633

ISBN: (纸本)9783319662633;9783319662626

The presence of symmetry in Boolean satisfiability (SAT) problem instances often poses challenges to solvers. Currently, the most effective approach to handle symmetry is by static symmetry breaking, which generates asymmetric constraints to add to the instance. An alternative way is to handle symmetry dynamically during solving. As modern SAT solvers can be viewed as propositional proof generators, adding a symmetry rule in a solver's proof system would be a straightforward technique to handle symmetry dynamically. However, none of these proposed symmetrical learning techniques are competitive to static symmetry breaking. In this paper, we present symmetric explanation learning, a form of symmetrical learning based on learning symmetric images of explanation clauses for unit propagations performed during search. A key idea is that these symmetric clauses are only learned when they would restrict the current search state, i.e., when they are unit or conflicting. We further provide a theoretical discussion on symmetric explanation learning and a working implementation in a state-of-the-art SAT solver. We also present extensive experimental results indicating that symmetric explanation learning is the first symmetrical learning scheme competitive with static symmetry breaking.

关键词： Boolean satisfiability Symmetry Proof theory Symmetric learning Dynamic symmetry breaking

来源：评论

学校读者我要写书评

暂无评论

A review of literature on parallel constraint solving

arXiv

引用

arXiv 2018年

作者： Gent, Ian P. McCreesh, Ciaran Miguel, Ian Moore, Neil C.A. Nightingale, Peter Prosser, Patrick Unsworth, Chris School of Computer Science University of St.Andrews St.AndrewsKY16 9SX United Kingdom School of Computing Science University of Glasgow GlasgowG12 8RZ United Kingdom School of Computer Science University of St.Andrews St.AndrewsKY16 9SX United Kingdom Adobe Systems Incorporated Edinburgh United Kingdom School of Computer Science University of St.Andrews St.AndrewsKY16 9SX United Kingdom School of Computing Science University of Glasgow GlasgowG12 8RZ United Kingdom 13 Grasmere Drive YorkYO10 3RY United Kingdom

As multicore computing is now standard, it seems irresponsible for constraints researchers to ignore the implications of it. Researchers need to address a number of issues to exploit parallelism, such as: Investigating which constraint algorithms are amenable to parallelisation;whether to use shared memory or distributed computation;whether to use static or dynamic decomposition;and how to best exploit portfolios and cooperating search. We review the literature, and see that we can sometimes do quite well, some of the time, on some instances, but we are far from a general solution. Yet there seems to be little overall guidance that can be given on how best to exploit multicore computers to speed up constraint solving. We hope at least that this survey will provide useful pointers to future researchers wishing to correct this situation. Under consideration in theory and practice of logic programming (TPLP. Copyright © 2018, The Authors. All rights reserved.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Bridging Static and Dynamic Program Analysis using Fuzzy logic 15

Bridging Static and Dynamic Program Analysis using Fuzzy Log...

引用

15th Workshop on Quantitative Aspects of programming Languages and Systems (QAPL) / European Joint Conferences on theory and practice of Software (ETAPS)

作者： Lidman, Jacob Svenningsson, Josef Chalmers Univ Technol Gothenburg Sweden

Static program analysis is used to summarize properties over all dynamic executions. In a unifying approach based on 3-valued logic properties are either assigned a definite value or unknown. But in summarizing a set of executions, a property is more accurately represented as being biased towards true, or towards false. Compilers use program analysis to determine benefit of an optimization. Since benefit (e.g., performance) is justified based on the common case understanding bias is essential in guiding the compiler. Furthermore, successful optimization also relies on understanding the quality of the information, i.e. the plausibility of the bias. If the quality of the static information is too low to form a decision we would like a mechanism that improves dynamically. We consider the problem of building such a reasoning framework and present the fuzzy data-flow analysis. Our approach generalize previous work that use 3-valued logic. We derive fuzzy extensions of data-flow analyses used by the lazy code motion optimization and unveil opportunities previous work would not detect due to limited expressiveness. Furthermore we show how the results of our analysis can be used in an adaptive classifier that improve as the application executes.

关键词： Fuzzy logic

来源：评论

学校读者我要写书评

暂无评论

Integrating ILP and SMT for Shortwave Radio Broadcast Resource Allocation and Frequency Assignment 23rd

Integrating ILP and SMT for Shortwave Radio Broadcast Resour...

引用

作者： Pan, Linjie Jin, Jiwei Gao, Xin Sun, Wei Ma, Feifei Yin, Minghao Zhang, Jian Chinese Acad Sci Inst Software State Key Lab Comp Sci Beijing Peoples R China Northeast Normal Univ Coll Comp Sci Changchun Peoples R China Chinese Acad Sci Lab Parallel Software & Computat Sci Inst Software Beijing Peoples R China Univ Chinese Acad Sci Beijing Peoples R China State Adm Press Publicat Radio Film & Televis Peo Adm Bur Radio Stn Beijing Peoples R China Shan Dong Jiaotong Univ Jinan Peoples R China

ISBN: (纸本)9783319661582;9783319661575

Shortwave radio broadcasting is the principal way for broadcasting of voice in many countries. The broadcasting quality of a radio program is determined not only by the parameters of the transmission device, but also by the radio frequency. In order to optimize the overall broadcasting quality, it is desirable to designate both devices and frequencies to radio programs, subject to various constraints including the non-interference of radio programs. In this paper, we propose a two-phase approach to this constrained optimization problem. It integrates ILP and SMT solving, as well as a local search algorithm. These methods are evaluated using real data, and the results are promising.

关键词： Integer Linear programming Satisfiability modulo theories Shortwave radio broadcast

来源：评论

学校读者我要写书评

暂无评论

Fundamental proof methods in computer science :

引用

2017年

作者： Konstantine Arkoudas David Rea Musser

ISBN: (纸本)9780262035538

A textbook that teaches students to read and write proofs using Athena. Proof is the primary vehicle for knowledge generation in mathematics. In computer science, proof has found an additional use: verifying that a particular system (or component, or algorithm) has certain desirable properties. This book teaches students how to read and write proofs using Athena, a freely downloadable computer language. Athena proofs are machine-checkable and written in an intuitive natural-deduction style. The book contains more than 300 exercises, most with full solutions. By putting proofs into practice, it demonstrates the fundamental role of logic and proof in computer science as no other existing text does. Guided by examples and exercises, students are quickly immersed in the most useful high-level proof methods, including equational reasoning, several forms of induction, case analysis, proof by contradiction, and abstraction/specialization. The book includes auxiliary material on SAT and SMT solving, automated theorem proving, and logic programming. The book can be used by upper undergraduate or graduate computer science students with a basic level of programming and mathematical experience. Professional programmers, practitioners of formal methods, and researchers in logic-related branches of computer science will find it a valuable reference.

关键词： Computer science Proof theory

来源：评论

学校读者我要写书评

暂无评论

Applications of Foundational Proof Certificates in theorem proving

Applications of Foundational Proof Certificates in theorem p...

引用

作者： Roberto Blanco Martinez Ecole polytechnique

学位级别：博士

Formal trust in an abstract property, be it a mathematical result or a quality of the behavior of a computer program or a piece of hardware, is founded on the existence of a proof of its correctness. Many different kinds of proofs are written by mathematicians or generated by theorem provers, with the common problem of ascertaining whether those claimed proofs are themselves correct. The recently proposed Foundational Proof Certificate (FPC) framework harnesses advances in proof theory to define the semantics of proof formats, which can be verified by an independent and trusted proof checking kernel written in a logic programming language. This thesis extends initial results in certification of first-order proofs in several directions. It covers various essential logical axes grouped in meaningful combinations as they occur in practice: first, classical logic without fixed points and proofs generated by automated theorem provers; later, intuitionistic logic with fixed points and equality as logical connectives and proofs generated by proof assistants. The role of proof certificates is no longer limited to representing complete proofs to enable independent checking, but is extended to model proof transformations where details can be added to or subtracted from a certificate. These transformations yield operationally simpler certificates, around which increasingly trustworthy and performant proof checkers are constructed. Another new role of proof certificates is writing high-level proof outlines, which can be used to represent standard proof patterns as written by mathematicians, as well as automated techniques like property-based testing. We apply these developments to fully certify results produced by two families of standard automated theorem provers: resolution- and satisfiability-based. Another application is the design of programmable proof description langages for a proof assistant.

关键词： automated theorem proving computational logic foundational proof certificates proof assistants proof theory proof outlines

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：