Please use this space to recognize any and all collaborations which assisted you on the completion of this assignment.
mathematical logic代写
Let $p$ and $q$ be propositional variables, and define the following rules of inference on propositional formulas using only $p, q$, and the logical symbols:
(R1) $\langle\varnothing, \varphi\rangle$ if $\varphi$ is a tautology.
(R2) $\langle{p}, q\rangle$
Prove that the deductive system with no axioms and the rules of inference described above does not have a Deduction Theorem.
Solve following by hand using the simplex method (20 pts each):
$$
\begin{aligned}
\max \quad 6 x_{1}+8 x_{2}+5 x_{3}+9 x_{4} \
\text { s.t. } \quad 2 x_{1}+x_{2}+x_{3}+3 x_{4} \leq 5 \
x_{1}+3 x_{2}+x_{3}+2 x_{4} \leq 3 \
x_{1}, x_{2}, x_{3}, x_{4} \geq 0
\end{aligned}
$$
$$
\begin{aligned}
\max \quad x_{1}+3 x_{2} & \
\text { s.t. }-x_{1}-x_{2} & \leq-3 \
&-x_{1}+x_{2} & \leq-1 \
& x_{1}+2 x_{2} & \leq 4 \
x_{1}, x_{2} & \geq 0
\end{aligned}
$
Let $\mathscr{L}:=\left{f^{2}, c\right}$ be a language including a binary function and a constant, and let $\mathrm{T}_{\mathrm{G}}$ be the set of sentences
- $(\forall x)(\forall y)(\forall z)(=f f x y z f x f y z)$
- $(\forall x)(=f x c x)$
- $(\forall x)(=f \operatorname{cxx})$
- $(\forall x)(\exists y)(=f x y c \quad \wedge=f y x c)$
Prove that $\mathrm{T}_{\mathrm{G}} \forall(\forall x)(\forall y)(=f x y f y x)$. (Hint: Soundness.)
real analysis代写analysis 2, analysis 3请认准UprivateTA™. UprivateTA™为您的留学生涯保驾护航。
金融代写
概率论代考
离散数学代写
E0 205 Mathematical Logic and Theorem Proving
Instructors: Deepak D’Souza and Kamal Lodaya
Teaching Assistants: P. Habeeb and Stanly Samuel.
- Motivation and ObjectivesThis course is about mathematical logic with a focus on automated reasoning techniques that are useful in reasoning about programs. In the first part of the course we cover Propositional and First-Order logic and some of the classical results like sound and complete proof systems, compactness, and decidability of the satisfiability/validity problems. In the second part we focus on decision procedures for various theories that arise while reasoning about assertions in programs.
- Course Outline
- Zeroth-Order/Propositional Logic:
- Proofs in arithmetic
- Propositional logic, proof
- Decision procedure, completeness and compactness
- First-Order Logic:
- Proof systems
- Undecidability
- Completeness and compactness
- Theories and Decision Procedures:
- Equality and Uninterpreted Functions (EUF)
- Linear Arithmetic
- Nelson-Oppen combination
- Array logics
- Constrained Horn Clauses
- Zeroth-Order/Propositional Logic:
- Meeting Schedule
- Lectures
- (24-Feb-2021) Course Overview: Mathematical Logic, Decision Procedures + Course Logistics. Recording Part 1, Recording Part 2
- (01-Mar-2021) Zeroeth-Order Logic: Syntax. [Slides] [Recording Part 1] [Recording Part 2].
- (03-Mar-2021) Zoroeth-Order Logic: Models. [Slides] [Recording]
- (08-Mar-2021) Zoroeth-Order Logic: Theories to Models. [Slides] [Recording]
- (10-Mar-2021) Intro to Propositional Logic. [Slides] [Recording]
- (15-Mar-2021) Consistency. [Slides] [Recording]
- (17-Mar-2021) Completeness. [Slides] [Recording]
- (22-Mar-2021) Decidability / Resolution. [Slides] [Recording]
- (24-Mar-2021 and 29-Mar-2021) DPLL Satisfiability Procedure. [Slides] [Whiteboard notes [Recording 24 Mar] [Recording 29 Mar]
- (31-Mar-2021) First Order Logic. [Slides] [Recording]
- (05-Apr-2021) First Order Logic (Proof System). [Slides] [Recording]
- (07-Apr-2021) First Order Logic (Universal Fragment). [Slides] [Recording]
- (12-Apr-2021) First Order Logic (Existential Fragment). [Slides] [Recording]
- (19-Apr-2021) Theories to Models. [Slides] [Recording]
- (26,28-Apr-2021 and 03-May-2021) Equality and Uninterpreted Functions (EUF). [Slides] [Recording 26-Apr-2021] [Recording 28-Apr-2021] [Recording 03-May-2021]
- (05, 10, 12-May-2021) Linear Arithmetic. [Slides] [Recording 05-May-2021, Part 1] [Recording 05-May-2021, Part 2] [Recording 10-May-2021] [Recording 12-May-2021]
- (17, 19-May-2021) Array Logic. [Slides] [Recording 19-May-2021]
- (24-May-2021) Constrained Horn Clauses (Sumanth Prabhu). [Slides] [Recording]
- (26-May-2021) Model-Based Projection (Stanly Samuel). [Slides] [Recording]
- (31-May-2021) Wrap-up lecture [Slides] [Recording]
- Books and other material
- First-order Logic and automated theorem proving, Melvin Fitting, Springer-Verlag, 1990.
- Logic for Computer Science — Foundations for Automatic Theorem Proving, Jean H. Gallier.
- Decision Procedures, Kroening and Strichman, Springer, 2008.
- The Calculus of Computation, Bradley and Manna, Springer, 2007.
- Computability and logic, George Boolos, John Burgess and Richard Jeffrey, Cambridge U Press, 2007.
- An Introduction to Logic, Madhavan Mukund and S P Suresh, Lecture Notes, Chennai Mathematical Institute (2011).
- Assignments
- Assignment 1 due by 2pm on Mon 15 March 2021.
- Assignment 2 due on Wed 14 April 2021.
- Assignment 3 Q1,2,3 due on Mon 10 May (Tutorial on 07-May-2021 slides on Python/Z3, example code. [Recording 06-May-2021], [Recording 10-May-2021].)
- Assignment 4 due on Mon 31 May 2021.
- Seminar Topics
- Decision Procedure for Real Arithmetic (Seidenberg and Tarski) (Mohith and Upamanyu, 10am Tue 11th May) Slides.
- Bit Vector Arithmetic (Kroening-Stichman (2e) Ch~6). Nabarun and Prathamesh (10am Tue 18th May). Slides.
- Maximal Specification Synthesis (Albarghouthi, Dillig, Gurfinkel, POPL 2016) (Logical Abduction). Alvin (10am, Tue 25th May).
- Undecidability of First-Order Logic (Reference: Boolos, Burgess, and Jeffrey) K. Sreehari (10am, Tue 1st June)
- A Linear-Time algorithm for Horn SAT (Dowling and Gallier, J. Logic Programming 1984 Link to paper). Sai Sanjeev and Shreepranav (3:30pm, Wed 2nd June). Slides.
- Uninterpreted Programs (Mathur, Madhusudan, Vishwanathan, PoPL 2019). Ajinkya (10am, Thu 3rd June)
- Decision Procedure for Presburger Logic (Reference: Boolos, Burgess, and Jeffrey). Gaurish and Prashik (3:30pm, Wed 9th June).
- E-Matching for Quantified Formulas (Greg Nelson PhD thesis (1980), De Moura and Bjorner CADE 2007)
- Weightage for evaluation:
- Mid-semester Exam: 20%
- Assignments + Quizes + Seminar: 40%
- Final Exam: 40%
- Exam Schedule:
- Mid-semester Exam: 3:30pm Wed 21st April 2021.
- Final Exam: 3:30pm Fri, 04 June 2021.
