Logic Engineering (1)
Bijan Parsia
Logic Engineering?
- Our KR formalims are logic
based
- Many
many logics
- A logic is
- a
syntax (set of well formed formulae)
- a semantics
(an interpretation function from formulae to structures)
- a
proof procedure (i.e., a set of validities)
- Not
every logic is apt for KR!
Basic Considerations
- Representational adequacy
- Weak
Cognitive adequacy
- Computationally
sensible
- Useful
services!
- We will focus on reasoning.
Why reasoning?
- Why representation!
- Information
systems
- Remember, richer information
- But
“richer” only makes sense with better services
- KR
as (partial) theory of intelligent reasoning
- Correlatively
of representation and reasoning
- Also,
- Representation
is difficult
- Good to have tools to work
with them
- Representations can quickly grow beyond
our best capabilties
Automated Reasoning
- (More specifically: “theorem proving”)
- Interactive
reasoning:
- A human
user interacts with the program to generate proofs
- System
provides verification of steps, suggested next steps, etc.
- (Fully)
Automated Reasoning
- Set up
initial conditions
- Premises,
question to be answered
AR in KR
- What's your goal?
- Prove
or verify math theorems
- Things
which are v. hard to prove
- Whenever you concern is
more for the answer than the process, AR is desirable
IR v. Interactive System
- Interactive reasoning refers to the process
of proving
- Human intervention is required
to supply
proof steps
- AR can
be part of an interactive system
- E.g.,
a dialogue driven expert system
- Consider database
based systems
- Consider Protege!
Some Considerations
- Designing (or selecting) a logic from a reasoning
perspective
- What's your core service?
- What
are the key services?
- Are you
interactive or not?
- What's the scale you need to
deal with?
- And other performance
characteristics
- What do you know about
implementation?
- What these somewhat
neglect
- Many surface syntax issues
Satisfiability and Entailment
- Many logical services
- Classification,
concept satisfiability, explanation, query answering
- Often
inter-reducible
- C is satisfiable iff a:C
is consistent for an aribtrary "a"
- C is
unsatisfiable iff C
\sqsubseteq \bot
- Satisfiability
is generally a core service
- With
entailment close behind
- Entailment by refutation
- \Gamma \models \alpha iff
\Gamma \cup \{\neg
\alpha\} is unsatisfiable
Decidability
- For every question, can we answer YES or NO in a
finite number of steps
- Correctly!
- That
is, is the problem mechanically solvable
- Propositional
logic is decidable
- First
order logic is semi-decidable
- Will
terminate on all YES answers
- Programming languages
are like this
- Why/when does this matter?
Complexity
- How much time (or space)?
- Complexity
of problem vs. of algorithm
- How
hard is the problem?
- How efficient
is the algorithm?
- "Worst
case" complexity (WCC)
- How much time will
we use if everything goes wrong.
- WWC_{problem} \leq WWC_{algorithm}
- WWC
doesn't tell you everything
- I.e.,
behavior in most cases, best case,
"typical" cases, "realisitc" cases, your case!
Complexity 2
Complexity
2
Complexity 3
Two Major AR PTs
- Resolution
- Invented
by J. A. Robinson (1965)
- Common
for propositional and FOL and logic programming systems
- Semantic
Tableaux
- Stems from Gentzen sequent
calculi
- First(?) used by Prawtiz for ATP
- Dominant
for model and description logics
Propositional Case
- Relatively simple
- Expressive enough for many
tasks
- Verification tasks
- Planning
problems
- Serious SAT solver industry
- Computationally
challenging enough
- Propositional
part of other interesting logics
Proof Procedure
- To test satisfiabiliy
- If
unsatisfiable, conclude the negation
- Refutation
procedure!
- Variant of indirect proof