CASC
2006
Springer
14 years 2 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
14 years 2 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
14 years 2 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
14 years 2 months ago
2009
Springer
ITP
2010
14 years 2 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
14 years 2 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
14 years 2 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
14 years 2 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
14 years 2 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
14 years 2 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...