NDLI: Automated Synthesis of Some Algorithms on Finite Sets

Content Provider	IEEE Xplore Digital Library
Author	Dramnesc, I. Jebelean, T.
Copyright Year	2012
Abstract	We start from the set theory axioms and we represent sets by monotone lists (sorted lists without duplications). For this, we define a representation function R and its reverse S and we want to synthesize the implementation of the essential corresponding predicates and functions over sets. Each synthesis starts as an inductive constructive proof which applies specific strategies and inference rules. We synthesize (by extracting from proofs) five algorithms among which two predicates: membership and inclusion, and three functions: union, intersection, and difference. In the process of proving we use properties from the theory of sets and we also add other necessary properties in the knowledge base. In this way we explore the theory of sets (represented as monotone lists). The program synthesis and the corresponding theory exploration are carried out in the frame of the Theorem a system. One of the major advantages of our approach is that the algorithms for operating on sets represented as monotone lists are more efficient than the ones for operating on sets represented as non-sorted lists.
Starting Page	143
Ending Page	151
File Size	270716
Page Count	9
File Format	PDF
ISBN	9781467350266
DOI	10.1109/SYNASC.2012.43
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2012-09-26
Publisher Place	Romania
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Context Theorema Scientific computing induction Knowledge based systems Educational institutions Set theory Inference algorithms Electronic mail proof techniques extraction algorithm synthesis
Content Type	Text
Resource Type	Article

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

Proof Techniques for Synthesis of Sorting Algorithms

Theory exploration of sets represented as monotone lists

Discovery of inductive algorithms through automated reasoning: A case study on sorting

Combinatorial Techniques for Proof-Based Synthesis of Sorting Algorithms

Rough sets model based on partition

Combinatorial Techniques for Proof-Based Synthesis of Sorting Algorithms

Fuzzy Qualitative Behaviour Prioritisation

Some new operations of soft sets

Approximate Reduction Algorithm Based on Rough Set Theory

Automated Synthesis of Some Algorithms on Finite Sets

Similar Documents

Proof Techniques for Synthesis of Sorting Algorithms

Theory exploration of sets represented as monotone lists

Discovery of inductive algorithms through automated reasoning: A case study on sorting

Combinatorial Techniques for Proof-Based Synthesis of Sorting Algorithms

Rough sets model based on partition

Combinatorial Techniques for Proof-Based Synthesis of Sorting Algorithms

Fuzzy Qualitative Behaviour Prioritisation

Some new operations of soft sets

Approximate Reduction Algorithm Based on Rough Set Theory

Automated Synthesis of Some Algorithms on Finite Sets