\documentclass[12pt]{article}
\usepackage{amsfonts}

\voffset=-3.0cm
\hoffset=-2.6cm
\textwidth=17.5cm
\textheight=24cm

\renewcommand{\not}{\neg}
\renewcommand{\and}{\wedge}
\renewcommand{\or}{\vee}
\newcommand{\impl}{\Rightarrow}
\newcommand{\lequiv}{\Leftrightarrow} %equivalence as logical connective
\newcommand{\all}{\forall}
\newcommand{\exi}{\exists}
\newcommand{\elc}{\models}  % semantic logical consequence
\newcommand{\ylc}{\vdash}  % syntactic logical consequence
%\equiv is already defined for === semantic equivalence
\newcommand{\union}{\cup}
\newcommand{\intersect}{\cap}
\newcommand{\true}{{\mathbb{T}}}
\newcommand{\false}{{\mathbb{F}}}
\newcommand{\nov}[1]{{\overline #1}}

\pagestyle{empty}

\begin{document}

{\bf Computational Logic, WS 2018.
Homework 7, given Dec. 3, due Dec 10.}

\bigskip

\noindent
1.
Find the sequent calculus rules for equivalence (in the assumptions and in the goals) by using
$$ \varphi \lequiv \psi\ \equiv\ (\varphi \and \psi) \or (\not \varphi \and \not \psi) $$ and the rules for negation, conjunction, and disjunction.

\bigskip

\noindent
2.
Express the sequent rules for disjunction over sets. Study the cases when the set is empty.

\bigskip

\noindent
3.
Prove by sequent calculus:
$$ (A \impl C) \and (B \impl C) \ylc (A \or B) \impl C.$$

\bigskip

\noindent
4.
Prove by sequent calculus:
$$ (A \or B) \impl C\ \ylc\ (A \impl C) \and (B \impl C).$$

\bigskip

\noindent
5.
Express formally the definition of continuity of a real function of real argument.

\end{document}

 
