Quantifier elimination by dependency sequents

DOI10.1007/s10703-014-0214-zzbMath1311.03061arXiv1201.5653OpenAlexW2065384342MaRDI QIDQ479823

Panagiotis Manolios, Eugene Goldberg

Publication date: 5 December 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1201.5653

zbMATH Keywords

quantifier eliminationmodel checkingresolutionSATdependency sequents

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Quantifier elimination, model completeness, and related topics (03C10)

Related Items

$$\#\exists $$ SAT: Projected Model Counting ⋮ Quantifier elimination by dependency sequents

Uses Software

• Chaff
• PicoSAT
• QUBOS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Quantifier elimination by dependency sequents
• A satisfiability procedure for quantified Boolean formulae
• New methods for 3-SAT decision and worst-case analysis
• SAT-Based Model Checking without Unrolling
• Quantifier Elimination via Functional Composition
• Boundary Points and Resolution
• Graph-Based Algorithms for Boolean Function Manipulation
• SAT-Solving Based on Boundary Point Elimination
• Decomposable negation normal form
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing
• Computer Aided Verification