CASC
2006
Springer
13 years 10 months ago
2006
Springer
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...
CASC
2006
Springer
13 years 10 months ago
2006
Springer
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...
ADG
2006
Springer
13 years 10 months ago
2006
Springer
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...
CASC
2009
Springer
13 years 10 months ago
2009
Springer
ITP
2010
13 years 10 months ago
2010
The Isabelle Collections Framework (ICF) provides a unified framework for using verified collection data structures in Isabelle/HOL formalizations and generating efficient functi...
ITP
2010
13 years 10 months ago
2010
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 ...
ITP
2010
13 years 10 months ago
2010
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...
ITP
2010
13 years 10 months ago
2010
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...
ITP
2010
13 years 10 months ago
2010
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...
ITP
2010
13 years 10 months ago
2010
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...