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

Computed Tomography01:10

Computed Tomography

8.9K
Tomography refers to imaging by sections. Computed tomography (CT) is a non-invasive imaging technique that uses computers to analyze several cross-sectional X-rays to reveal minute details about structures in the body.
The technique was invented in the 1970s and is based on the principle that as X-rays pass through the body, they are absorbed or reflected at different levels. In the technique, a patient lies on a motorized platform while a computerized axial tomography (CAT) scanner rotates...
8.9K
Cancers Originate from Somatic Mutations in a Single Cell02:21

Cancers Originate from Somatic Mutations in a Single Cell

15.0K
Cancer arises from mutations in the critical genes that allow healthy cells to escape cell cycle regulation and acquire the ability to proliferate indefinitely. Though originating from a single mutation event in one of the originator cells, cancer progresses when the mutant cell lines continue to gain more and more mutations, and finally, become malignant. For example, chronic myelogenous leukemia (CML) develops initially as a non-lethal increase in white blood cells, which progressively...
15.0K
Design Example: Traverse Angle Computations01:25

Design Example: Traverse Angle Computations

345
Traverse angle computations are a critical component of surveying, used to compute the internal angles within a closed traverse. A traverse consists of a series of connected lines forming a closed loop, often used for land boundary delineation or mapping. Calculating the internal angles ensures accuracy in the traverse geometry and is essential for checking survey data integrity.The process begins with known azimuths and bearings of the traverse sides. Internal angles at each vertex are...
345
Area Computation by the Alternative Coordinate Method01:24

Area Computation by the Alternative Coordinate Method

670
The alternative coordinate method, also known as the Shoelace Formula, is a technique for determining the area of a traverse using Cartesian coordinates. This method relies on the sequential arrangement of x and y coordinates for each point of the shape, ensuring accuracy and ease of application.In this approach, each corner's x and y coordinates are listed as fractions, with the x-coordinate as the numerator and the y-coordinate as the denominator. These coordinates are arranged sequentially...
670
Imaging Studies III: Computed Tomography01:27

Imaging Studies III: Computed Tomography

410
DefinitionComputed Tomography (CT) of the genitourinary (GU) tract is a non-invasive imaging modality that utilizes X-rays and computer processing to generate detailed cross-sectional images of the urinary system, encompassing the kidneys, ureters, bladder, and adjacent structures such as the adrenal glands.PurposeCT scans of the GU tract serve several diagnostic and therapeutic purposes, including:Diagnosis of Urinary Tract Diseases: Detects kidney stones, tumors, cysts, and congenital...
410
The Role of Ion Channels in Neuronal Computation01:19

The Role of Ion Channels in Neuronal Computation

3.9K
A postsynaptic neuron usually receives numerous impulses from several other presynaptic neurons. The axon hillock of the postsynaptic neuron integrates all these signals and determines the likelihood of firing an action potential.
Sometimes a single EPSP is strong enough to induce an action potential in the postsynaptic neuron. However, multiple presynaptic inputs must often create EPSPs around the same time for the postsynaptic neuron to be sufficiently depolarized to fire an action potential....
3.9K

You might also read

Related Articles

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

Sort by
Same author

Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL.

Journal of automated reasoning·2020
See all related articles

Related Experiment Video

Updated: Feb 13, 2026

High-precision Electromagnetic Flowmeter with Empty Pipe Detection via Complex Programmable Logic Device-based Waveform Recognition
05:11

High-precision Electromagnetic Flowmeter with Empty Pipe Detection via Complex Programmable Logic Device-based Waveform Recognition

Published on: June 27, 2025

711

Computational logic: its origins and applications.

Lawrence C Paulson1

  • 1Computer Laboratory, University of Cambridge, Cambridge CB3 0FD, UK.

Proceedings. Mathematical, Physical, and Engineering Sciences
|March 7, 2018
PubMed
Summary

Computational logic uses computers for formal reasoning, evolving from mathematical logic studies. Advanced tools like Isabelle enhance proof construction for hardware, software, and mathematical verification.

Keywords:
Isabelleformal verificationlogic for computable functionsproof assistantstheorem proving

More Related Videos

Application of Deep Learning-Based Medical Image Segmentation via Orbital Computed Tomography
04:48

Application of Deep Learning-Based Medical Image Segmentation via Orbital Computed Tomography

Published on: November 30, 2022

3.5K
Using Phylogenetic Analysis to Investigate Eukaryotic Gene Origin
08:57

Using Phylogenetic Analysis to Investigate Eukaryotic Gene Origin

Published on: August 14, 2018

16.6K

Related Experiment Videos

Last Updated: Feb 13, 2026

High-precision Electromagnetic Flowmeter with Empty Pipe Detection via Complex Programmable Logic Device-based Waveform Recognition
05:11

High-precision Electromagnetic Flowmeter with Empty Pipe Detection via Complex Programmable Logic Device-based Waveform Recognition

Published on: June 27, 2025

711
Application of Deep Learning-Based Medical Image Segmentation via Orbital Computed Tomography
04:48

Application of Deep Learning-Based Medical Image Segmentation via Orbital Computed Tomography

Published on: November 30, 2022

3.5K
Using Phylogenetic Analysis to Investigate Eukaryotic Gene Origin
08:57

Using Phylogenetic Analysis to Investigate Eukaryotic Gene Origin

Published on: August 14, 2018

16.6K

Area of Science:

  • Computer Science
  • Formal Logic
  • Mathematical Reasoning

Background:

  • Computational logic emerged from 19th-century efforts to formalize mathematical reasoning.
  • It involves using computers to establish facts within logical systems.
  • The field encompasses diverse formalisms, techniques, and technologies.

Purpose of the Study:

  • To outline the evolution and applications of computational logic.
  • To highlight advancements in automated reasoning and proof construction.
  • To showcase the expanding use of computational logic in mathematics.

Main Methods:

  • Exploration of the 'logic for computable functions' (LCF) approach.
  • Introduction of Isabelle as a refinement of LCF, offering enhanced automation and flexibility.
  • Application of interactive proof construction and user-assisted code for verification.

Main Results:

  • Development of sophisticated tools like Isabelle for logical formalisms.
  • Successful application of computational logic in verifying hardware and software correctness.
  • Increasing adoption of these techniques within the field of mathematics itself.

Conclusions:

  • Computational logic provides powerful tools for rigorous verification.
  • Isabelle represents a significant advancement in automated theorem proving.
  • The scope of computational logic is expanding beyond computer science into pure mathematics.