First-order Logic
First-order logic is "classical" logic. Each sentence is true or
false, and quantification is allowed so that you can say things like,
"For all x, if x is a dog, then x has a tail." There is a unary
negation operator and standard connectives are used: conjunction,
disjunction and implication.
Determining whether or not a first-order theory is consistent ("has a
model", in slightly more technical terms) is in general semidecidable.
This means that there are algorithms that are guaranteed to terminate
with the answer "yes" if the theory is consistent, but might never
terminate if the theory is inconsistent. There can be no algorithm
that will always terminate in both cases.
CIRL
While the compact syntax of first-order logic makes it
attractive, its computational properties are inappropriate for fielded
systems. We work on finding ways to achieve both the syntax of
first-order methods and the computational features of other languages.
Parent areas:
Language
Subareas:
Quantified propositional logic
Back to the CIRL Overview Page.