Abstract
First-order constraints over arbitrary theories or structures can be formalised as the formula instantiation problem as defined in [11]. Several re- suits have been previously obtained for the formula instantiation problem in the case of quantifier-free formulas of first-order logic. In this paper we prove the first general result on formula instantiation for quantified formulas, namely that formula instantiation is decidable for the monadic class without equality. © Springer-Verlag Berlin Heidelberg 2005.
| Original language | English |
|---|---|
| Title of host publication | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci. |
| Publisher | Springer Nature |
| Pages | 132-138 |
| Number of pages | 6 |
| Volume | 2605 |
| ISBN (Print) | 3540250514, 9783540250517 |
| Publication status | Published - 2005 |
| Event | Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday - Duration: 1 Jan 1824 → … http://dblp.uni-trier.de/db/conf/birthday/siekmann2005.html#ChubarovV05http://dblp.uni-trier.de/rec/bibtex/conf/birthday/ChubarovV05.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/birthday/ChubarovV05 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|
Conference
| Conference | Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday |
|---|---|
| Period | 1/01/24 → … |
| Internet address |