Paper Info
Title
Model Generation for Horn Logic with Stratified Negation
Abstract
Model generation is an important formal technique for finding interesting instances of computationally hard problems. In this paper we study model generation over Horn logic under the closed world assumption extended with stratified negation. We provide a novel three-stage algorithm that solves this problem: First, we reduce the relevant Horn clauses to a set of non-monotonic predicates. Second, we apply a fixed-point procedure to these predicates that reveals candidate solutions to the model generation problem. Third, we encode these candidates into a satisfiability problem that is evaluated with a state-of-the-art SMT solver. Our algorithm is implemented, and has been successfully applied to key problems arising in model-based design.
Year
DOI
Venue
2008
10.1007/978-3-540-68855-6_1
FORTE
Keywords
Field
DocType
satisfiability problem,model generation,key problem,computationally hard problem,stratified negation,relevant horn clause,novel three-stage algorithm,candidate solution,closed world assumption,model generation problem,horn logic,software development,model based design
ENCODE,Horn clause,Negation,Computer science,Boolean satisfiability problem,Theoretical computer science,Horn logic,Predicate (grammar),Closed-world assumption,Satisfiability modulo theories
Conference
Volume
ISSN
Citations 
5048
0302-9743
10
PageRank 
References 
Authors
0.60
14
2
Name
Order
Citations
PageRank
Ethan K. Jackson120415.30
Wolfram Schulte22342153.40