We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.
We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.
Published online by Cambridge University Press: 30 September 2009
We've considered various algorithms (tableaux, resolution, etc.) for verifying that a first-order formula is logically valid, if indeed it is. But these will not in general tell us when a formula is not valid. We'll see in Chapter 7 that there is no systematic procedure for doing so. However, there are procedures that work for certain special classes of formulas, or for validity in certain special (classes of) models, and we discuss some of the more important ones in this chapter. Often these naturally generalize common decision problems in mathematics and universal algebra such as equation-solving or the ‘word problem’.
The decision problem
There are three natural and closely connected problems for first-order logic for which we might want an algorithmic solution. By negating the formula, we can according to taste present them in terms of validity or unsatisfiability.
Confirm that a logically valid (or unsatisfiable) formula is indeed valid (resp. unsatisfiable), and never confirm an invalid (satisfiable) one.
Confirm that a logically invalid (or satisfiable) formula is indeed invalid (resp. satisfiable), and never confirm a valid (unsatisfiable) one.
Test whether a formula is valid or invalid (or whether it is satisfiable or unsatisfiable).
Evidently (3) encompasses both (1) and (2). Conversely, solutions to both (1) and (2) could be used together to solve (3): just run the verification procedures for validity and invalidity (or satisfiability and unsatisfiability) in parallel. Now, we have presented explicit solutions to (1), such as tableaux or resolution. But these do not solve (3). Given a satisfiable formula, these algorithms, while at least not incorrectly claiming they are unsatisfiable, will not always terminate.
To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.
Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.
Find out more about the Kindle Personal Document Service.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.
