| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 6873954 | Information and Computation | 2015 | 18 Pages |
Abstract
We demonstrate that the satisfiability problem for a fragment of HRELTL allows for a satisfiability-preserving reduction to RELTL(RA), a logic over discrete traces with atoms in non-linear Real Arithmetic for which automated reasoning procedures are being developed.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Alessandro Cimatti, Marco Roveri, Stefano Tonetta,