David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
Studia Logica 93 (2/3):147 - 180 (2009)
In the current paper we consider theories with vocabulary containing a number of binary and unary relation symbols. Binary relation symbols represent labeled edges of a graph and unary relations represent unique annotations of the graph's nodes. Such theories, which we call annotation theories^ can be used in many applications, including the formalization of argumentation, approximate reasoning, semantics of logic programs, graph coloring, etc. We address a number of problems related to annotation theories over finite models, including satisfiability, querying problem, specification of preferred models and model checking problem. We show that most of considered problems are NPTime- or co-NPTime-complete. In order to reduce the complexity for particular theories, we use second-order quantifier elimination. To our best knowledge none of existing methods works in the case of annotation theories. We then provide a new second-order quantifier elimination method for stratified theories, which is successful in the considered cases. The new result subsumes many other results, including those of [2, 28, 21]
|Keywords||argumentation theory labeled graphs annotations semantics of logic programs second-order quantifier elimination|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
John McCarthy (1980). Circumscription — A Form of Non-Monotonic Reasoning. Artificial Intelligence 13:27–39.
Patrick Blackburn & Jerry Seligman (1995). Hybrid Languages. Journal of Logic, Language and Information 4 (3):251-272.
Martin W. A. Caminada & Dov M. Gabbay (2009). A Logical Account of Formal Argumentation. Studia Logica 93 (2-3):109-145.
Yining Wu, Martin Caminada & Dov M. Gabbay (2009). Complete Extensions in Argumentation Coincide with 3-Valued Stable Models in Logic Programming. Studia Logica 93 (2/3):383 - 403.
Valentin Goranko (2012). Temporal Logics with Reference Pointers and Computation Tree Logics. Journal of Applied Non-Classical Logics 10 (3-4):221-242.
Citations of this work BETA
Dov M. Gabbay (2009). Fibring Argumentation Frames. Studia Logica 93 (2/3):231 - 295.
Similar books and articles
Joseph Berger (2000). Theory and Formalization: Some Reflections on Experience. Sociological Theory 18 (3):482-489.
Ítala M. L. D'Ottaviano (1987). Definability and Quantifier Elimination for J3-Theories. Studia Logica 46 (1):37 - 54.
J. C. E. Dekker (1981). Twilight Graphs. Journal of Symbolic Logic 46 (3):539-571.
George Weaver (1988). Classifying ℵ0-Categorical Theories. Studia Logica 47 (4):327 - 345.
Robert E. Woodrow (1976). A Note on Countable Complete Theories Having Three Isomorphism Types of Countable Models. Journal of Symbolic Logic 41 (3):672-680.
Rolf Backofen, James Rogers & K. Vijay-Shanker (1995). A First-Order Axiomatization of the Theory of Finite Trees. Journal of Logic, Language and Information 4 (1):5-39.
James Loveys & Predrag Tanović (1996). Countable Models of Trivial Theories Which Admit Finite Coding. Journal of Symbolic Logic 61 (4):1279-1286.
M. Krynicki & K. Zdanowski (2005). Theories of Arithmetics in Finite Models. Journal of Symbolic Logic 70 (1):1-28.
Dov M. Gabbay & Andrzej Szałas (2007). Second-Order Quantifier Elimination in Higher-Order Contexts with Applications to the Semantical Analysis of Conditionals. Studia Logica 87 (1):37 - 50.
Ross Willard (1994). Hereditary Undecidability of Some Theories of Finite Structures. Journal of Symbolic Logic 59 (4):1254-1262.
Added to index2009-11-21
Total downloads10 ( #324,403 of 1,792,277 )
Recent downloads (6 months)4 ( #207,535 of 1,792,277 )
How can I increase my downloads?