National Repository of Grey Literature 1 records found  Search took 0.00 seconds. 

Warning: Requested record does not seem to exist.
Automated model building
Miček, Radek ; Stanovský, David (advisor) ; Surynek, Pavel (referee)
We implement a MACE-style method for finding finite models in unsorted classical first-order logic. Additionally to well-known modifications of the method we also describe and implement several new modifications such as: unflattening, generation of redundant clauses and encoding into Gecode constraints. Our implementation is benchmarked together with Mace4, Paradox and iProver. Finally, some suggestions for improvements and further research are given. Powered by TCPDF (www.tcpdf.org)

Interested in being notified about new results for this query?
Subscribe to the RSS feed.