Skip Navigation

Journal of Logic and Computation 1994 4(1):23-68; doi:10.1093/logcom/4.1.23
© 1994 by Oxford University Press
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by SIMMONS, H.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Original Articles

The Monotonous Elimination of Predicate Variables

HAROLD SIMMONS

Department of Computer Science, The University Manchester Ml3 9PL, UKE.mail: hsimmons{at}cs.man.ac.uk

I describe an algorithm which, when given a sentence {Gamma} involving universally quantified predicate variables, first reduces this sentence to a normal form {Gamma}* and then, if {Gamma}* satisfies certain extra restrictions, eliminates the predicate variables of {Gamma}* to produce a predicate-free equivalent of {Gamma}. This process may involve the introduction of skolem functions but in many cases does not (and so produces a more elementary version of {Gamma}). The algorithm eliminates the predicate variables by witnessing them with certain definable predicates. The choice of these predicates is guided by the shape of the normal form {Gamma}*. The algorithm was initially designed to deal with modal correspondence problems. In this respect it is an extension of Sahlqvist's algorithm which produces first-order equivalents of a wide class of modal formulas. The algorithm is illustrated by several examples from modal logic.

Keywords: Quantifier elimination; substitution method; lower-order equivalents


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.