https://cs.indstate.edu/web/index.php?action=history&feed=atom&title=CS_421_Formal_Methods 2026-04-14T16:13:47Z Revision history for this page on the wiki MediaWiki 1.44.0 https://cs.indstate.edu/web/index.php?title=CS_421_Formal_Methods&diff=81&oldid=prev 2025-08-17T13:22:12Z

<p>1 revision imported</p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="en"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 13:22, 17 August 2025</td> </tr><tr><td colspan="4" class="diff-notice" lang="en"><div class="mw-diff-empty">(No difference)</div> </td></tr> <!-- diff cache key wiki2:diff:1.41:old-80:rev-81 --> </table>

Jkinne https://cs.indstate.edu/web/index.php?title=CS_421_Formal_Methods&diff=80&oldid=prev 2021-05-18T12:59:38Z

<p>Created page with &quot;== Catalog Description == Elements of formal logic; various approaches to automation including resolution; restrictions and search methods; inductive theorem-proving; Knuth-B...&quot;</p> <p><b>New page</b></p><div>== Catalog Description ==<br /> <br /> Elements of formal logic; various approaches to automation including resolution; restrictions and search methods; inductive theorem-proving; Knuth-Bendix completion; Boyer-Moore theorem-prover; applications. Prerequisite - C or better in CS 202 and CS 303.<br /> <br /> == Prerequisites ==<br /> Student must have knowledge of Discrete Structures<br /> <br /> <br /> <br /> == Standard Content ==<br /> ===Course Outline ===<br /> This is meant to be a “Logic in Computer Science” course.<br /> The main topics covered are Propositional and First Order Logic Syntax and Semantics,proofs of valid arguments via resolution are stressed. Invalidity of arguments is demonstrated through the building of models for the premises and negated conclusions. The use of Automated Reasoning programs such as the OTTER theorem prover and MACE2 model builder is shown.<br /> Reasoning with equality , is discussed using equality theories and paramodulation.<br /> Reasoning in Inductive Theories is covered.<br /> Applications covered are: Program Analysis, Design of Logic Circuits, Plan Generation,Question Answering, Answer Extraction, and Logical Foundations of Databases.<br /> <br /> ===Learning Outcomes===<br /> A knowledge of deductive logic and its applications in Computer Science.<br /> <br /> <br /> ===Important Assignments and/or Exam Questions===<br /> Assignments include chapter summaries of textbook chapters, and use of theorem provers and model builders ; pencil and paper quizzes are given over the course content.<br /> <br /> === Standard resources ===<br /> Symbolic Logic and Mechanical Theorem Proving by C-L Chang and R.C.T. Lee (Academic Press, 1973, ISBN-10: 0-12-170350-9)</div>

wiki_previous>Znoble1