Informatics Report Series



Related Pages

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

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]
Publication Type:Conference Paper Publication Status:Published
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
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 = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh