Automatická konstrukce modelů
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 constrai...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Dissertation |
| Language: | Czech |
| Published: |
2015
|
| Online Access: | http://www.nusl.cz/ntk/nusl-350826 |