Informatics Report Series


Report   

EDI-INF-RR-1342


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:On Locally Minimal Nullstellensatz Proofs
Authors: Leonardo de Moura ; Grant Passmore
Date:Sep 2009
Publication Title:Satisfiability Modulo Theories (SMT) 2009 [co-located with CADE-22]
Publisher:ACM
Publication Type:Conference Paper Publication Status:Published
Abstract:
Hilbert's weak Nullstellensatz guarantees the existence of algebraic proof objects certifying the unsatisfiability of systems of polynomial equations not satisfiable over any algebraically closed field. Such proof objects take the form of ideal membership identities and can be found algorithmically using Groebner bases and cofactor-based linear algebra techniques. However, these proof objects may contain redundant information: a proper subset of the equational assumptions used in these proofs may be sufficient to derive the unsatisfiability of the original polynomial system. For using Nullstellensatz techniques in SMT-based decision methods, a minimal proof object is often desired. With this in mind, we introduce a notion of locally minimal Nullstellensatz proofs and give ideal-theoretic algorithms for their construction.
Links To Paper
1st Link
Bibtex format
@InProceedings{EDI-INF-RR-1342,
author = { Leonardo de Moura and Grant Passmore },
title = {On Locally Minimal Nullstellensatz Proofs},
book title = {Satisfiability Modulo Theories (SMT) 2009 [co-located with CADE-22]},
publisher = {ACM},
year = 2009,
month = {Sep},
url = {http://research.microsoft.com/en-us/um/people/leonardo/MSR-TR-2009-90.pdf},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh