6 Combination of decision procedures (1185842)
Текст из файла
ECE750T-28:Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures forCombination TheoriesVijay Ganesh(Original notes from Isil Dillig)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories1/44MotivationISo far, learned about decision procedures for useful theoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories2/44MotivationISo far, learned about decision procedures for useful theoriesIExamples: Theory of equality with uninterpreted functions, theory ofrationals, theory of integersVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories2/44MotivationISo far, learned about decision procedures for useful theoriesIExamples: Theory of equality with uninterpreted functions, theory ofrationals, theory of integersIBut in many cases, we need to decide satisfiability of formulas involvingmultiple theoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories2/44MotivationISo far, learned about decision procedures for useful theoriesIExamples: Theory of equality with uninterpreted functions, theory ofrationals, theory of integersIBut in many cases, we need to decide satisfiability of formulas involvingmultiple theoriesIExample: 1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories2/44MotivationISo far, learned about decision procedures for useful theoriesIExamples: Theory of equality with uninterpreted functions, theory ofrationals, theory of integersIBut in many cases, we need to decide satisfiability of formulas involvingmultiple theoriesIExample: 1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)IThis formula does not belong to any individual theoryVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories2/44MotivationISo far, learned about decision procedures for useful theoriesIExamples: Theory of equality with uninterpreted functions, theory ofrationals, theory of integersIBut in many cases, we need to decide satisfiability of formulas involvingmultiple theoriesIExample: 1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)IThis formula does not belong to any individual theoryIBut it does belong, for instance, to combination of T= and TZVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories2/44OverviewIRecall: Given two theories T1 and T2 that have the = predicate, we definea combined theory T1 ∪ T2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories3/44OverviewIRecall: Given two theories T1 and T2 that have the = predicate, we definea combined theory T1 ∪ T2ISignature of T1 ∪ T2 : Σ1 ∪ Σ2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories3/44OverviewIRecall: Given two theories T1 and T2 that have the = predicate, we definea combined theory T1 ∪ T2ISignature of T1 ∪ T2 : Σ1 ∪ Σ2IAxioms of T1 ∪ T2 : A1 ∪ A2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories3/44OverviewIRecall: Given two theories T1 and T2 that have the = predicate, we definea combined theory T1 ∪ T2ISignature of T1 ∪ T2 : Σ1 ∪ Σ2IAxioms of T1 ∪ T2 : A1 ∪ A2IGiven decision procedures for T1 and T2 , we want a decision procedure todecide satisfiability of formulas in T1 ∪ T2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories3/44OverviewIRecall: Given two theories T1 and T2 that have the = predicate, we definea combined theory T1 ∪ T2ISignature of T1 ∪ T2 : Σ1 ∪ Σ2IAxioms of T1 ∪ T2 : A1 ∪ A2IGiven decision procedures for T1 and T2 , we want a decision procedure todecide satisfiability of formulas in T1 ∪ T2IToday’s lecture: Learn about Nelson-Oppen method for constructingdecision procedure for combined theory T1 ∪ T2 from individual decisionprocedures for T1 and T2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories3/44Nelson-Oppen OverviewVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories4/44Nelson-Oppen OverviewIThis method also allows combining arbitrary number of theoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories4/44Nelson-Oppen OverviewIThis method also allows combining arbitrary number of theoriesIFor instance, to combine T1 , T2 , T3 , first combine T1 , T2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories4/44Nelson-Oppen OverviewIThis method also allows combining arbitrary number of theoriesIFor instance, to combine T1 , T2 , T3 , first combine T1 , T2IThen, combine T1 ∪ T2 and T3 again using Nelson-OppenVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories4/44Nelson-Oppen OverviewIThis method also allows combining arbitrary number of theoriesIFor instance, to combine T1 , T2 , T3 , first combine T1 , T2IThen, combine T1 ∪ T2 and T3 again using Nelson-OppenIHowever, Nelson-Oppen imposes some restrictions on theories that can becombinedVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories4/44Restrictions of Nelson-OppenINelson-Oppen method imposes the following restrictions: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 fragmentsVijay 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 DNFVijay 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 = {=}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.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
