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

Theorems of Pappus and Guldinus: Problem Solving01:12

Theorems of Pappus and Guldinus: Problem Solving

828
Pappus and Guldinus's theorems are powerful mathematical principles that are used for finding the surface area and volume of composite shapes. For example, consider a cylindrical storage tank with a conical top. Finding the surface area or volume can be challenging for such complex shapes. These theorems are particularly useful in calculating the volume and surface area of such systems. Here, the cylindrical storage tank with a conical top can be broken down into two simple shapes: a...
828
Second Uniqueness Theorem01:16

Second Uniqueness Theorem

1.1K
Consider a region consisting of several individual conductors with a definite charge density in the region between these conductors. The second uniqueness theorem states that if the total charge on each conductor and the charge density in the in-between region are known, then the electric field can be uniquely determined.
In contrast, consider that the electric field is non-unique and apply Gauss's law in divergence form in the region between the conductors and the integral form to the...
1.1K
Thevinin's Theorem01:15

Thevinin's Theorem

881
Thévenin's theorem plays a pivotal role in electrical circuit analysis, offering a solution to the challenges posed by variable loads within a circuit. In practical applications, it is common to encounter circuits where certain elements remain fixed while others fluctuate, often referred to as the "load." A typical household electrical outlet serves as a prime example of a variable load, as it can be connected to a variety of appliances, each with its own unique electrical...
881
Norton's Theorem01:14

Norton's Theorem

864
Norton's theorem is a fundamental principle stating that a linear two-terminal circuit can be substituted with an equivalent circuit, which comprises a current source (ⅠN) in parallel with a resistor (RN). Here, ⅠN represents the short-circuit current flowing through the terminals, and RN stands for the input or equivalent resistance at the terminals when all independent sources are deactivated. This implies that the circuit illustrated in Figure (a) can be exchanged with the...
864
Castigliano's Theorem: Problem Solving01:14

Castigliano's Theorem: Problem Solving

797
The deflection of a simply supported beam that carries a central point load can be analyzed using structural mechanics principles, particularly by applying Castigliano's theorem. This theorem relates the displacement at the load application point to the partial derivatives of the strain energy in the structure. The simply supported beam with a point load at its center has symmetric reaction forces at the supports, each bearing half of the load. The bending moment at any point along the beam...
797
Castigliano's Theorem01:18

Castigliano's Theorem

574
Castigliano's theorem analyzes displacements and rotations in elastic structures. It relates the derivative of elastic strain energy to the applied forces or moments, allowing for the calculation of deformations. The theorem states that the partial derivative of the total strain energy of a system with respect to a specific load results in the displacement at the point where the load is applied. This principle applies to both forces and moments.
574

You might also read

Related Articles

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

Sort by
Same author

Building Strategies into QBF Proofs.

Journal of automated reasoning·2021
Same journal

Combining Higher-Order Logic with Set Theory Formalizations.

Journal of automated reasoning·2023
Same journal

Synthesising Programs with Non-trivial Constants.

Journal of automated reasoning·2023
Same journal

Unifying Splitting.

Journal of automated reasoning·2023
Same journal

First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification.

Journal of automated reasoning·2023
Same journal

A Formalization of SQL with Nulls.

Journal of automated reasoning·2022
Same journal

A Comprehensive Framework for Saturation Theorem Proving.

Journal of automated reasoning·2022
See all related articles

Related Experiment Video

Updated: Oct 5, 2025

Quantum State Engineering of Light with Continuous-wave Optical Parametric Oscillators
09:23

Quantum State Engineering of Light with Continuous-wave Optical Parametric Oscillators

Published on: May 30, 2014

14.7K

Proof Complexity of Modal Resolution.

Sarah Sigley1, Olaf Beyersdorff2

  • 1School of Computing, University of Leeds, Leeds, UK.

Journal of Automated Reasoning
|January 24, 2022
PubMed
Summary
This summary is machine-generated.

We introduce new methods to analyze the efficiency of modal resolution systems, proving their equivalence and establishing the first lower bounds for modal proof complexity using Prover-Delayer games.

Keywords:
Lower boundsModal logicPigeonhole principleProof complexityProver–Delayer gamesResolution

More Related Videos

Examining Online Syntactic Processing of Spoken Complex Sentences in Chinese Using Dual-Modal Interference Tasks
08:32

Examining Online Syntactic Processing of Spoken Complex Sentences in Chinese Using Dual-Modal Interference Tasks

Published on: September 5, 2019

5.7K
Generation and Coherent Control of Pulsed Quantum Frequency Combs
06:42

Generation and Coherent Control of Pulsed Quantum Frequency Combs

Published on: June 8, 2018

9.1K

Related Experiment Videos

Last Updated: Oct 5, 2025

Quantum State Engineering of Light with Continuous-wave Optical Parametric Oscillators
09:23

Quantum State Engineering of Light with Continuous-wave Optical Parametric Oscillators

Published on: May 30, 2014

14.7K
Examining Online Syntactic Processing of Spoken Complex Sentences in Chinese Using Dual-Modal Interference Tasks
08:32

Examining Online Syntactic Processing of Spoken Complex Sentences in Chinese Using Dual-Modal Interference Tasks

Published on: September 5, 2019

5.7K
Generation and Coherent Control of Pulsed Quantum Frequency Combs
06:42

Generation and Coherent Control of Pulsed Quantum Frequency Combs

Published on: June 8, 2018

9.1K

Area of Science:

  • * Theoretical Computer Science
  • * Mathematical Logic
  • * Artificial Intelligence

Background:

  • * Modal resolution systems are foundational for modal theorem proving.
  • * Existing systems by Nalon and Dixon, and Nalon et al. form the basis of current modal theorem proving techniques.
  • * Understanding the proof complexity of these systems is crucial for advancing automated reasoning.

Purpose of the Study:

  • * To analyze and compare the proof complexity of existing modal resolution systems.
  • * To introduce a new, tighter variant of modal resolution.
  • * To develop a novel technique for establishing lower bounds in modal proof complexity.

Main Methods:

  • * Efficient translation of proofs between different modal resolution variants.
  • * Development of Prover-Delayer games for modal lower bounds.
  • * Introduction of a new modal pigeonhole principle to illustrate the lower bound technique.
  • * Comparison with modal Frege systems.

Main Results:

  • * All investigated modal resolution systems are equivalent from a proof complexity perspective.
  • * The first lower bound technique for modal resolution using Prover-Delayer games is established.
  • * Exponential-size proofs are required for the new modal pigeonhole principle in modal resolution.
  • * A genuine modal separation between modal resolution and modal Frege systems is achieved.

Conclusions:

  • * The study provides a comprehensive analysis of modal resolution proof complexity.
  • * New techniques offer a way to establish genuine modal lower bounds.
  • * The findings contribute to a deeper understanding of the expressive power and limitations of modal logics in automated reasoning.