Sciweavers

CASC
2006
Springer
128views Mathematics» more  CASC 2006»
14 years 3 months ago
New Domains for Applied Quantifier Elimination
We address various aspects of our computer algebra-based computer logic system redlog. There are numerous examples in the literature for successful applications of redlog to practi...
Thomas Sturm
CASC
2006
Springer
100views Mathematics» more  CASC 2006»
14 years 3 months ago
Reducing Computational Costs in the Basic Perturbation Lemma
Homological Perturbation Theory [11, 13] is a well-known general method for computing homology, but its main algorithm, the Basic Perturbation Lemma, presents, in general, high com...
Ainhoa Berciano, María José Jim&eacu...
ADG
2006
Springer
191views Mathematics» more  ADG 2006»
14 years 3 months ago
Automatic Verification of Regular Constructions in Dynamic Geometry Systems
We present an application of an automatic theorem proving (ATP) in the verification of constructions made with dynamic geometry software (DGS). Given a specification language for g...
Predrag Janicic, Pedro Quaresma
ITP
2010
179views Mathematics» more  ITP 2010»
14 years 3 months ago
The Isabelle Collections Framework
The Isabelle Collections Framework (ICF) provides a unified framework for using verified collection data structures in Isabelle/HOL formalizations and generating efficient functi...
Peter Lammich, Andreas Lochbihler
ITP
2010
140views Mathematics» more  ITP 2010»
14 years 3 months ago
Case-Analysis for Rippling and Inductive Proof
Abstract. Rippling is a heuristic used to guide rewriting and is typically used for inductive theorem proving. We introduce a method to support case-analysis within rippling. Like ...
Moa Johansson, Lucas Dixon, Alan Bundy
ITP
2010
114views Mathematics» more  ITP 2010»
14 years 3 months ago
A New Foundation for Nominal Isabelle
Pitts et al introduced a beautiful theory about names and binding based on the notions of permutation and support. The engineering challenge is to smoothly adapt this theory to a t...
Brian Huffman, Christian Urban
ITP
2010
164views Mathematics» more  ITP 2010»
14 years 3 months ago
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
Nitpick is a counterexample generator for Isabelle/HOL that builds on Kodkod, a SAT-based first-order relational model finder. Nitpick supports unbounded quantification, (co)ind...
Jasmin Christian Blanchette, Tobias Nipkow
ITP
2010
172views Mathematics» more  ITP 2010»
14 years 3 months ago
Equations: A Dependent Pattern-Matching Compiler
Abstract. We present a compiler for definitions made by pattern matching on inductive families in the Coq system. It allows to write structured, recursive dependently-typed functi...
Matthieu Sozeau
ITP
2010
165views Mathematics» more  ITP 2010»
14 years 3 months ago
A Mechanized Translation from Higher-Order Logic to Set Theory
Abstract. In order to make existing formalizations available for settheoretic developments, we present an automated translation of theories from Isabelle/HOL to Isabelle/ZF. This c...
Alexander Krauss, Andreas Schropp