Validating Mathematical Theories and Algorithms with RISCAL

Wolfgang Schreiner

doi:10.1007/978-3-319-96812-4_21

Validating Mathematical Theories and Algorithms with RISCAL

Wolfgang Schreiner

Research Institute for Symbolic Computation

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

RISCAL is a language for describing mathematical algo- rithms and formally specifying their behavior with respect to user-defined theories in first-order logic. This language is based on a type system that constrains the size of all types by formal parameters; thus a RISCAL specification denotes an infinite class of models of which every instance has finite size. This allows the RISCAL software to fully automatically check in small instances the validity of theorems and the correctness of algorithms. Our goal is to quickly detect errors respectively inadequa- cies in the formalization by falsification in small model instances before attempting actual correctness proofs for the whole model class. [NOTE: The final authenticated version is available online at Springer]

Original language	English
Title of host publication	Intelligent Computer Mathematics
Editors	F. Rabe, W. Farmer, G. Passmore, A. Youssef
Place of Publication	Berlin
Publisher	Springer
Pages	248-254
Number of pages	7
Volume	11006
ISBN (Print)	978-3-319-96811-7
DOIs	https://doi.org/10.1007/978-3-319-96812-4_21
Publication status	Published - 2018

Publication series

Name	Lecture Notes in Artificial Intelligence (LNAI)

Fields of science

101 Mathematics
101001 Algebra
101005 Computer algebra
101009 Geometry
101012 Combinatorics
101013 Mathematical logic
101020 Technical mathematics

JKU Focus areas

Computation in Informatics and Mathematics

Access to Document

10.1007/978-3-319-96812-4_21

Cite this

@inproceedings{b05ada5606954578981711126ac7f689,

title = "Validating Mathematical Theories and Algorithms with RISCAL",

abstract = "RISCAL is a language for describing mathematical algo- rithms and formally specifying their behavior with respect to user-defined theories in first-order logic. This language is based on a type system that constrains the size of all types by formal parameters; thus a RISCAL specification denotes an infinite class of models of which every instance has finite size. This allows the RISCAL software to fully automatically check in small instances the validity of theorems and the correctness of algorithms. Our goal is to quickly detect errors respectively inadequa- cies in the formalization by falsification in small model instances before attempting actual correctness proofs for the whole model class. [NOTE: The final authenticated version is available online at Springer]",

author = "Wolfgang Schreiner",

year = "2018",

doi = "10.1007/978-3-319-96812-4_21",

language = "English",

isbn = "978-3-319-96811-7",

volume = "11006",

series = "Lecture Notes in Artificial Intelligence (LNAI)",

publisher = "Springer",

pages = "248--254",

editor = "{F. Rabe, W. Farmer, G. Passmore, A. Youssef}",

booktitle = "Intelligent Computer Mathematics",

}

TY - GEN

T1 - Validating Mathematical Theories and Algorithms with RISCAL

AU - Schreiner, Wolfgang

PY - 2018

Y1 - 2018

N2 - RISCAL is a language for describing mathematical algo- rithms and formally specifying their behavior with respect to user-defined theories in first-order logic. This language is based on a type system that constrains the size of all types by formal parameters; thus a RISCAL specification denotes an infinite class of models of which every instance has finite size. This allows the RISCAL software to fully automatically check in small instances the validity of theorems and the correctness of algorithms. Our goal is to quickly detect errors respectively inadequa- cies in the formalization by falsification in small model instances before attempting actual correctness proofs for the whole model class. [NOTE: The final authenticated version is available online at Springer]

AB - RISCAL is a language for describing mathematical algo- rithms and formally specifying their behavior with respect to user-defined theories in first-order logic. This language is based on a type system that constrains the size of all types by formal parameters; thus a RISCAL specification denotes an infinite class of models of which every instance has finite size. This allows the RISCAL software to fully automatically check in small instances the validity of theorems and the correctness of algorithms. Our goal is to quickly detect errors respectively inadequa- cies in the formalization by falsification in small model instances before attempting actual correctness proofs for the whole model class. [NOTE: The final authenticated version is available online at Springer]

U2 - 10.1007/978-3-319-96812-4_21

DO - 10.1007/978-3-319-96812-4_21

M3 - Conference proceedings

SN - 978-3-319-96811-7

VL - 11006

T3 - Lecture Notes in Artificial Intelligence (LNAI)

SP - 248

EP - 254

BT - Intelligent Computer Mathematics

A2 - F. Rabe, W. Farmer, G. Passmore, A. Youssef, null

PB - Springer

CY - Berlin

ER -