6 Combination of decision procedures (Презентации лекций), страница 2

Signatures can only share equality: Σ1 ∩ Σ2 = {=}4. Theories T1 and T2 must be stably infiniteVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories5/44Restrictions of Nelson-OppenINelson-Oppen method imposes the following restrictions:1. Only allows combining quantifier-free fragments2. Only allows combining formulas without disjunctions, but not a majorlimitation because can convert to DNF3. Signatures can only share equality: Σ1 ∩ Σ2 = {=}4. Theories T1 and T2 must be stably infiniteITheory T is stably infinite iff every satisfiable qff formula is satisfiable in auniverse of discourse with infinite cardinalityVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories5/44Restrictions of Nelson-OppenINelson-Oppen method imposes the following restrictions:1.

Only allows combining quantifier-free fragments2. Only allows combining formulas without disjunctions, but not a majorlimitation because can convert to DNF3. Signatures can only share equality: Σ1 ∩ Σ2 = {=}4. Theories T1 and T2 must be stably infiniteITheory T is stably infinite iff every satisfiable qff formula is satisfiable in auniverse of discourse with infinite cardinalityIIn other words, if qff F is satisfiable, then there exists T -model thatsatisfies F and has infinite cardinality.Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories5/44Restrictions of Nelson-OppenINelson-Oppen method imposes the following restrictions:1.

Only allows combining quantifier-free fragments2. Only allows combining formulas without disjunctions, but not a majorlimitation because can convert to DNF3. Signatures can only share equality: Σ1 ∩ Σ2 = {=}4. Theories T1 and T2 must be stably infiniteITheory T is stably infinite iff every satisfiable qff formula is satisfiable in auniverse of discourse with infinite cardinalityIIn other words, if qff F is satisfiable, then there exists T -model thatsatisfies F and has infinite cardinality.IThus, theories with only finite models are not stably infinite.Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories5/44Example of Non-Stably Infinite TheorySignature :Axiom :Vijay Ganesh(Original notes from Isil Dillig),{a, b, =}∀x .

x = a ∨ x = bECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories6/44Example of Non-Stably Infinite TheorySignature :Axiom :I{a, b, =}∀x . x = a ∨ x = bAxiom says that any object in the universe of discourse must be equal toeither a or bVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories6/44Example of Non-Stably Infinite TheorySignature :Axiom :{a, b, =}∀x .

x = a ∨ x = bIAxiom says that any object in the universe of discourse must be equal toeither a or bINow consider U containing more than 2 elementsVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories6/44Example of Non-Stably Infinite TheorySignature :Axiom :{a, b, =}∀x . x = a ∨ x = bIAxiom says that any object in the universe of discourse must be equal toeither a or bINow consider U containing more than 2 elementsIThen, there is at least one element distinct from both a and bVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories6/44Example of Non-Stably Infinite TheorySignature :Axiom :{a, b, =}∀x .

x = a ∨ x = bIAxiom says that any object in the universe of discourse must be equal toeither a or bINow consider U containing more than 2 elementsIThen, there is at least one element distinct from both a and bIThus, any U with more than 2 elements violates axiomVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories6/44Example of Non-Stably Infinite TheorySignature :Axiom :{a, b, =}∀x . x = a ∨ x = bIAxiom says that any object in the universe of discourse must be equal toeither a or bINow consider U containing more than 2 elementsIThen, there is at least one element distinct from both a and bIThus, any U with more than 2 elements violates axiomIHence, theory only has finite models, and is not stably infiniteVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories6/44Examples of Stably Infinite TheoriesIFortunately, almost any theory of interest is stably infiniteVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories7/44Examples of Stably Infinite TheoriesIFortunately, almost any theory of interest is stably infiniteIAll theories we discussed, T= , TQ , TZ , TA , are stably infiniteVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories7/44Examples of Stably Infinite TheoriesIFortunately, almost any theory of interest is stably infiniteIAll theories we discussed, T= , TQ , TZ , TA , are stably infiniteIWhich of these theories can we combine using Nelson-Oppen?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories7/44Examples of Stably Infinite TheoriesIFortunately, almost any theory of interest is stably infiniteIAll theories we discussed, T= , TQ , TZ , TA , are stably infiniteIWhich of these theories can we combine using Nelson-Oppen?1.

T= and TQ ?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories7/44Examples of Stably Infinite TheoriesIFortunately, almost any theory of interest is stably infiniteIAll theories we discussed, T= , TQ , TZ , TA , are stably infiniteIWhich of these theories can we combine using Nelson-Oppen?1. T= and TQ ? yesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories7/44Examples of Stably Infinite TheoriesIFortunately, almost any theory of interest is stably infiniteIAll theories we discussed, T= , TQ , TZ , TA , are stably infiniteIWhich of these theories can we combine using Nelson-Oppen?1.

T= and TQ ? yes2. T= and TZ ?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories7/44Examples of Stably Infinite TheoriesIFortunately, almost any theory of interest is stably infiniteIAll theories we discussed, T= , TQ , TZ , TA , are stably infiniteIWhich of these theories can we combine using Nelson-Oppen?1. T= and TQ ? yes2.

T= and TZ ? yesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories7/44Examples of Stably Infinite TheoriesIFortunately, almost any theory of interest is stably infiniteIAll theories we discussed, T= , TQ , TZ , TA , are stably infiniteIWhich of these theories can we combine using Nelson-Oppen?1. T= and TQ ? yes2.

T= and TZ ? yes3. TA and TZ ?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories7/44Examples of Stably Infinite TheoriesIFortunately, almost any theory of interest is stably infiniteIAll theories we discussed, T= , TQ , TZ , TA , are stably infiniteIWhich of these theories can we combine using Nelson-Oppen?1. T= and TQ ? yes2. T= and TZ ? yes3. TA and TZ ? yesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories7/44Examples of Stably Infinite TheoriesIFortunately, almost any theory of interest is stably infiniteIAll theories we discussed, T= , TQ , TZ , TA , are stably infiniteIWhich of these theories can we combine using Nelson-Oppen?1. T= and TQ ? yes2.

T= and TZ ? yes3. TA and TZ ? yesIIn general, almost any theory we care about can be combined usingNelson-OppenVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories7/44Examples of Stably Infinite TheoriesIFortunately, almost any theory of interest is stably infiniteIAll theories we discussed, T= , TQ , TZ , TA , are stably infiniteIWhich of these theories can we combine using Nelson-Oppen?1.

T= and TQ ? yes2. T= and TZ ? yes3. TA and TZ ? yesIIn general, almost any theory we care about can be combined usingNelson-OppenVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories7/44Examples of Stably Infinite TheoriesIFortunately, almost any theory of interest is stably infiniteIAll theories we discussed, T= , TQ , TZ , TA , are stably infiniteIWhich of these theories can we combine using Nelson-Oppen?1. T= and TQ ? yes2. T= and TZ ? yes3. TA and TZ ? yesIIn general, almost any theory we care about can be combined usingNelson-OppenIMore recent work has also extended Nelson-Oppen to non-stably-infinitetheoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories7/44Nelson-Oppen OverviewINelson-Oppen method has conceptually two-different phases:Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories8/44Nelson-Oppen OverviewINelson-Oppen method has conceptually two-different phases:1.