A CDCL-Style Calculus for Solving Non-linear Constraints
- Submitting institution
-
The University of Manchester
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 129466060
- Type
- E - Conference contribution
- DOI
-
10.1007/978-3-030-29007-8_8
- Title of conference / published proceedings
- Frontiers of Combining Systems, 12th International Symposium : FroCoS 2019, Proceedings
- First page
- 131
- Volume
- 11715
- Issue
- -
- ISSN
- 1611-3349
- Open access status
- Compliant
- Month of publication
- August
- Year of publication
- 2019
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
3
- Research group(s)
-
A - Computer Science
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- "Addresses highly challenging problem of solving non-linear constraints involving transcendental functions. Such constraints are used in applications, e.g. verification of hybrid systems, and verification of deep mathematical proofs such as the proof of Kepler''s conjecture by Thomas C. Hales.
Best Paper at the International Symposium on Frontiers of Combining Systems.
Invited talks:
- Deduktionstreffen (42nd German Conference On Artificial Intelligence, 2019)
- Workshop on Logic and Search (Lisbon, 2019).
Enabled industrial funding from Intel (USD336,000)."
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
