Experiments in Automatic Theorem Proving.

Abstract

The experiments described in this report are proofs in EKL of properties of different LISP programs operating on different representations of the same mathematical structures - finite permutations. EKL is an interactive proof checker based upon the language of higher order logic, higher order unification and a decision procedure for a fragment of first order logic. The following questions are asked: What representations of mathematical structure and facts are better suited for formalization and also simultaneously applicable to many different contexts? What methods and strategies will make it possible to prove automatically an extensive body of mathematical knowledge? Can higher order logic be conveniently applied to proofs of elementary facts?

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 1986
Accession Number
ADA327449

Entities

People

  • Gianluigi Bellin
  • Jussi Ketonen

Organizations

  • Stanford University

Tags

Communities of Interest

  • Biomedical
  • C4I
  • Ground and Sea Platforms
  • Space

DTIC Thesaurus Topics

  • Abstracts
  • Automatic
  • Coast Guard
  • Commerce
  • Computer Programs
  • Computer Science
  • Computers
  • Construction
  • Electronic Mail
  • Formal Languages
  • Language
  • Mathematics
  • Permutations
  • Schools
  • Security
  • Set Theory
  • Virtual Reality

Readers

  • Mathematical Modeling and Probability Theory.
  • Systems Analysis and Design