Lazy Theorem Proving for Bounded Model Checking over Infinite Domains

2002 ◽  
pp. 438-455 ◽  
Author(s):  
Leonardo de Moura ◽  
Harald Rueß ◽  
Maria Sorea
Keyword(s):  
Model Checking ◽  
Theorem Proving ◽  
Bounded Model Checking ◽  
Infinite Domains

Bounded Model Checking for Probabilistic Computation Tree Logic

2012 ◽  
Vol 23 (7) ◽  
pp. 1656-1668 ◽  
Author(s):  
Cong-Hua ZHOU ◽  
Zhi-Feng LIU ◽  
Chang-Da WANG
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Probabilistic Computation ◽  
Computation Tree Logic ◽  
Computation Tree

scholarly journals Symbolic Causality Checking Using Bounded Model Checking

2015 ◽  
pp. 203-221 ◽  
Author(s):  
Adrian Beer ◽  
Stephan Heidinger ◽  
Uwe Kühne ◽  
Florian Leitner-Fischer ◽  
Stefan Leue
Keyword(s):  
Model Checking ◽  
Bounded Model Checking

scholarly journals Preface

2011 ◽  
Vol 21 (4) ◽  
pp. 671-677 ◽  
Author(s):  
GÉRARD HUET
Keyword(s):  
Mathematical Logic ◽  
Computer Science ◽  
20Th Century ◽  
Theorem Proving ◽  
Propositional Calculus ◽  
Interactive Theorem Proving ◽  
Predicate Calculus ◽  
Special Issue ◽  
Mathematical Structures ◽  
Infinite Domains

This special issue of Mathematical Structures in Computer Science is devoted to the theme of ‘Interactive theorem proving and the formalisation of mathematics’.The formalisation of mathematics started at the turn of the 20th century when mathematical logic emerged from the work of Frege and his contemporaries with the invention of the formal notation for mathematical statements called predicate calculus. This notation allowed the formulation of abstract general statements over possibly infinite domains in a uniform way, and thus went well beyond propositional calculus, which goes back to Aristotle and only allowed tautologies over unquantified statements.

Sign in / Sign up

Export Citation Format

Share Document