This project, establishing a deductive software repository, aims at making software more available, reliable, durable, higher quality, uniform. Deductive software consists of symbolic routines for logical manipulations including decision procedures, solvers, rewriters, model checkers, and theorem provers. It serves as the semantic foundation for many scientific and engineering applications in areas such as hardware and software verification, program synthesis and analysis, data- and knowledge-based systems, artificial intelligence, linguistics, and e-commerce. This work outlines an initiative for deductive software components called QPQ ("quid pro quo") as a marketplace for publishing, exchanging, and refining deductive software components. The refereed publication and distribution of such scientific software components in open source often yields higher quality, greater visibility, and accelerated productivity. Efficient implementation of deductive algorithms, an extremely complex and delicate task, requires serious investment in basic infrastructure such as concrete and abstract syntax, syntactic tools (parsers, typecheckers, pretty-printer), primitive operations (substitution, matching, unification, normalization), and advanced operations (constraint satisfaction, forward and backward chaining, rewriting, simplification, decision procedures, induction methods). Potential impacts include availability, reliability, quality, durability, productivity, visibility, uniformity, synergy, serendipity, and history. The following principles will be employed in running the repository: authenticity, uniqueness, access, relevance, format, quality and version control, and academic credit. QPQ is already recognized as a valuable resource for research and education in deductive software. With its role in facilitating the semantic web and through other applications of logico-symbolic computing, the QPQ repository might become crucial to society.
