The Tenth International Symposium on Artificial Intelligence and Mathematics pages:1-15
ISAIM edition:10 location:Fot Launderdale date:2-4 January 2008
First Order ID-Logic interprets general first order, non-monotone, inductive definability by generalizing the well-founded semantics for logic programs. We show that, for general (thus perhaps infinite)
structures, inference in First Order ID-Logic is complete Pi^1_2 over the natural numbers. We also prove a Skolem Theorem for the logic: every consistent formula of First Order ID-Logic has a countable model.