• Skip to primary navigation
  • Skip to main content
SRI InternationalSRI mobile logo

SRI International

SRI International - American Nonprofit Research Institute

  • About
    • Blog
    • Press room
  • Expertise
    • Advanced imaging systems
    • Artificial intelligence
    • Biomedical R&D services
    • Biomedical sciences
    • Computer vision
    • Cyber & formal methods
    • Education and learning
    • Innovation strategy and policy
    • National security
    • Ocean & space
    • Quantum
    • QED-C
    • Robotics, sensors & devices
    • Speech & natural language
    • Video test & measurement
  • Ventures
  • NSIC
  • Careers
  • Contact
  • 日本支社
Show Search
Hide Search
Cyber & formal methods publications November 1, 2020

Deductive Synthesis of the Unification Algorithm: The Automation of Introspection

Richard J. Waldinger November 1, 2020

SRI Authors: Richard J. Waldinger

Citation

Copy to clipboard


Richard Waldinger. Logic and Practice of Programming (LPOP) 2020; In SPLASH 2020, the ACM SIGPLAN conference on Systems, Programming, Languages, and Applications: Software for Humanity.

Abstract

We are working to create the first automatic deductive synthesis of a unification algorithm. The program is extracted from a proof of the existence of an output substitution that satisfies a given logical specification. Tests are introduced via case analysis in the proof, and recursion by application of the mathematical induction principle. The automation of the proof is challenging because it combines full quantifier reasoning and induction in a single framework. The program obtained is simpler than those previously constructed manually. Improvements in theorem proving technology lead us to believe that deductive synthesis could become a viable part of software production. Also, we suggest that a theorem prover’s reasoning about itself can be regarded as a form of introspection, which may enable it to improve itself.

↓ View online

Share this

Facebooktwitterlinkedinmail

Cyber & formal methods publications, Publication

How can we help?

Once you hit send…

We’ll match your inquiry to the person who can best help you.

Expect a response within 48 hours.

Career call to action image

Make your own mark.

Search jobs
Our work

Case studies

Publications

Timeline of innovation

Areas of expertise

Blog

Institute

Leadership

Press room

Media inquiries

Compliance

Privacy policy

Careers

Job listings

Contact

SRI Ventures

Our locations

Headquarters

333 Ravenswood Ave
Menlo Park, CA 94025 USA

+1 (650) 859-2000

Subscribe to our newsletter

日本支社

SRI International

  • Contact us
  • Privacy Policy
  • Cookies
  • DMCA
  • Copyright © 2022 SRI International