SYBIL - A Mechanical Theorem Prover
The applications of mechanical theorem proving range over many types of problems. Program analysis, number theory, state transformation problems and question answering all fall within its theoretical capabilities. The basic methods for proving theorems is very simple, but their pure application puts most problems outside of physical possibility. In response to this, refinements, strategies and heuristics must be employed to reach the solution, without violating soundness or completeness in the process. SYBIL goes some small way to achieving this, and illustrates some of the difficulties.
SubjectsField of Research::08 - Information and Computing Sciences::0802 - Computation Theory and Mathematics::080203 - Computational Logic and Formal Languages
- Engineering: Reports