NDLI: Reasoning About Algebraic Data Types with Abstractions

Content Provider	Springer Nature Link
Author	Pham, Tuan Hung Gacek, Andrew Whalen, Michael W.
Copyright Year	2016
Abstract	Reasoning about functions that operate over algebraic data types is an important problem for a large variety of applications. One application of particular interest is network applications that manipulate or reason about complex message structures, such as XML messages. This paper presents a decision procedure for reasoning about algebraic data types using abstractions that are provided by catamorphisms: fold functions that map instances of algebraic data types to values in a decidable domain. We show that the procedure is sound and complete for a class of catamorphisms that satisfy a generalized sufficient surjectivity condition. Our work extends a previous decision procedure that unrolls catamorphism functions until a solution is found. We use the generalized sufficient surjectivity condition to address an incompleteness in the previous unrolling algorithm (and associated proof). We then propose the categories of monotonic and associative catamorphisms, which we argue provide a more intuitive inclusion test than the generalized sufficient surjectivity condition. We use these notions to address two open problems from previous work: (1) we provide a bound, with respect to formula size, on the number of unrollings necessary for completeness, showing that it is linear for monotonic catamorphisms and exponentially small for associative catamorphisms, and (2) we demonstrate that associative catamorphisms can be combined within a formula while preserving completeness. Our combination results extend the set of problems that can be reasoned about using the catamorphism-based approach. We also describe an implementation of the approach, called RADA, which accepts formulas in an extended version of the SMT-LIB 2.0 syntax. The procedure is quite general and is central to the reasoning infrastructure for Guardol, a domain-specific language for reasoning about network guards.
Starting Page	281
Ending Page	318
Page Count	38
File Format	PDF
ISSN	01687433
Journal	Journal of Automated Reasoning
Volume Number	57
Issue Number	4
e-ISSN	15730670
Language	English
Publisher	Springer Netherlands
Publisher Date	2016-03-29
Publisher Place	Dordrecht
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Decision procedures Algebraic data types SMT solvers Mathematical Logic and Formal Languages Artificial Intelligence (incl. Robotics) Mathematical Logic and Foundations Symbolic and Algebraic Manipulation
Content Type	Text
Resource Type	Article
Subject	Artificial Intelligence Computational Theory and Mathematics Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

A Decision Procedure for (Co)datatypes in SMT Solvers

Extending Sledgehammer with SMT Solvers

Decision Procedures for Flat Array Properties

An Approximation Framework for Solvers and Decision Procedures

The 2013 Evaluation of SMT-COMP and SMT-LIB

Implementing and Reasoning About Hash-consed Data Structures in Coq

A Tableau Decision Procedure for $\mathcal{SHOIQ}$

Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005)

Preface: Special Issue on Uncertain Reasoning

Reasoning About Algebraic Data Types with Abstractions

Similar Documents

A Decision Procedure for (Co)datatypes in SMT Solvers

Extending Sledgehammer with SMT Solvers

Decision Procedures for Flat Array Properties

An Approximation Framework for Solvers and Decision Procedures

The 2013 Evaluation of SMT-COMP and SMT-LIB

Implementing and Reasoning About Hash-consed Data Structures in Coq

A Tableau Decision Procedure for $\mathcal{SHOIQ}$

Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005)

Preface: Special Issue on Uncertain Reasoning

Reasoning About Algebraic Data Types with Abstractions