Jove
Visualize
Contact Us
JoVE
x logofacebook logolinkedin logoyoutube logo
ABOUT JoVE
OverviewLeadershipBlogJoVE Help Center
AUTHORS
Publishing ProcessEditorial BoardScope & PoliciesPeer ReviewFAQSubmit
LIBRARIANS
TestimonialsSubscriptionsAccessResourcesLibrary Advisory BoardFAQ
RESEARCH
JoVE JournalMethods CollectionsJoVE Encyclopedia of ExperimentsArchive
EDUCATION
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab ManualFaculty Resource CenterFaculty Site
Terms & Conditions of Use
Privacy Policy
Policies

Related Concept Videos

Social Exchange Theory02:06

Social Exchange Theory

40.8K
We have discussed why we form relationships, what attracts us to others, and different types of love. But what determines whether we are satisfied with and stay in a relationship? One theory that provides an explanation is social exchange theory. According to social exchange theory, we act as naïve economists in keeping a tally of the ratio of costs and benefits of forming and maintaining a relationship with others (Rusbult & Van Lange, 2003).
40.8K
Band Theory02:35

Band Theory

17.2K
When two or more atoms come together to form a molecule, their atomic orbitals combine and molecular orbitals of distinct energies result. In a solid, there are a large number of atoms, and therefore a large number of atomic orbitals that may be combined into molecular orbitals. These groups of molecular orbitals are so closely placed together to form continuous regions of energies, known as the bands.
The energy difference between these bands is known as the band gap.
Conductor, Semiconductor,...
17.2K
Scientific Laws and Theories02:31

Scientific Laws and Theories

89.0K
Scientific Laws
89.0K
Valence Bond Theory02:45

Valence Bond Theory

50.3K
Overview of Valence Bond Theory
50.3K
Valence Bond Theory02:42

Valence Bond Theory

11.3K
Coordination compounds and complexes exhibit different colors, geometries, and magnetic behavior, depending on the metal atom/ion and ligands from which they are composed. In an attempt to explain the bonding and structure of coordination complexes, Linus Pauling proposed the valence bond theory, or VBT, using the concepts of hybridization and the overlapping of the atomic orbitals. According to VBT, the central metal atom or ion (Lewis acid) hybridizes to provide empty orbitals of suitable...
11.3K
Attribution Theory00:56

Attribution Theory

13.8K
Behavior is a product of both the situation (e.g., cultural influences, social roles, and the presence of bystanders) and of the person (e.g., personality characteristics). Subfields of psychology tend to focus on one influence or behavior over others. Situationism is the view that our behavior and actions are determined by our immediate environment and surroundings. In contrast, dispositionism holds that our behavior is determined by internal factors (Heider, 1958).
13.8K

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by
Same authorSame journal

Combining Higher-Order Logic with Set Theory Formalizations.

Journal of automated reasoning·2023
Same author

Machine Learning Guidance for Connection Tableaux.

Journal of automated reasoning·2021
See all related articles

Related Experiment Video

Updated: Feb 7, 2026

qKAT: Quantitative Semi-automated Typing of Killer-cell Immunoglobulin-like Receptor Genes
07:58

qKAT: Quantitative Semi-automated Typing of Killer-cell Immunoglobulin-like Receptor Genes

Published on: March 6, 2019

9.1K

Hammer for Coq: Automation for Dependent Type Theory.

Łukasz Czajka1, Cezary Kaliszyk1

  • 1University of Innsbruck, Innsbruck, Austria.

Journal of Automated Reasoning
|August 3, 2018
PubMed
Summary
This summary is machine-generated.

This study introduces a novel hammer for automated theorem proving in dependent type theory, specifically for the Coq proof assistant. The system translates complex logic into first-order logic, enabling automated proof reconstruction and achieving significant success in library development emulation.

Keywords:
Calculus of inductive constructionsCoqHammerProof automation

More Related Videos

Semi-automated Analysis of Mouse Skeletal Muscle Morphology and Fiber-type Composition
08:36

Semi-automated Analysis of Mouse Skeletal Muscle Morphology and Fiber-type Composition

Published on: August 31, 2017

11.2K
Automated Acoustic Dispensing for the Serial Dilution of Peptide Agonists in Potency Determination Assays
08:06

Automated Acoustic Dispensing for the Serial Dilution of Peptide Agonists in Potency Determination Assays

Published on: November 10, 2016

8.0K

Related Experiment Videos

Last Updated: Feb 7, 2026

qKAT: Quantitative Semi-automated Typing of Killer-cell Immunoglobulin-like Receptor Genes
07:58

qKAT: Quantitative Semi-automated Typing of Killer-cell Immunoglobulin-like Receptor Genes

Published on: March 6, 2019

9.1K
Semi-automated Analysis of Mouse Skeletal Muscle Morphology and Fiber-type Composition
08:36

Semi-automated Analysis of Mouse Skeletal Muscle Morphology and Fiber-type Composition

Published on: August 31, 2017

11.2K
Automated Acoustic Dispensing for the Serial Dilution of Peptide Agonists in Potency Determination Assays
08:06

Automated Acoustic Dispensing for the Serial Dilution of Peptide Agonists in Potency Determination Assays

Published on: November 10, 2016

8.0K

Area of Science:

  • Formal Methods
  • Automated Theorem Proving
  • Dependent Type Theory

Background:

  • Hammers offer powerful automation for HOL and set theory proof assistants.
  • Advanced type theories like the Calculus of Inductive Constructions (CIC) lack robust hammer support due to translation challenges.

Purpose of the Study:

  • To present an architecture and implementation of a full hammer for dependent type theory within the Coq proof assistant.
  • To develop translation and proof reconstruction mechanisms for CIC-based systems.

Main Methods:

  • A novel translation from Coq's extensions of CIC to untyped first-order logic.
  • A proof reconstruction mechanism combining eauto-type algorithms, rewriting, congruence closure, and forward reasoning.
  • Machine learning for relevant premise selection.

Main Results:

  • The developed hammer successfully translates and reconstructs proofs for dependent type theory in Coq.
  • The system demonstrates practical utility, proving 40.8% of Coq standard library theorems in a bootstrapping scenario.
  • Automated proofs were achieved in approximately 40 seconds on an 8-CPU system.

Conclusions:

  • The implemented hammer provides a viable solution for automating proofs in dependent type theory systems like Coq.
  • The translation and reconstruction methods are effective for practical automated theorem proving.
  • This work advances the automation capabilities for advanced type theory proof assistants.