-
Impact of Extended Reality on Robot-Assisted Surgery Training
Authors:
Michael Bickford,
Fayez Alruwaili,
Sara Ragab,
Hanna Rothenberg,
Mohammad Abedin-Nasab
Abstract:
Robot Assisted Surgeries (RAS) have one of the steepest learning curves of any type of surgery. Because of this, methods to practice RAS outside the operating room have been developed to improve the surgeons skills. These strategies include the incorporation of extended reality simulators into surgical training programs. In this Systematic review, we seek to determine if extended reality simulator…
▽ More
Robot Assisted Surgeries (RAS) have one of the steepest learning curves of any type of surgery. Because of this, methods to practice RAS outside the operating room have been developed to improve the surgeons skills. These strategies include the incorporation of extended reality simulators into surgical training programs. In this Systematic review, we seek to determine if extended reality simulators can improve the performance of novice surgeons and how their performance compares to the conventional training of surgeons on Surgical robots. Using the PRISMA 2020 guidelines, a systematic review and meta-analysis was performed searching PubMed, Embase, Web of Science, and Cochrane library for studies that compared the performance of novice surgeons that received no additional training, trained with extended reality, or trained with inanimate physical simulators (conventional additional training). We included articles that gauged performance using either GEARS or Time to complete measurements and used SPSS to perform a meta-analysis to compare the performance outcomes of the surgeons after training. Surgeons trained using extended reality completed their surgical tasks statistically significantly faster than those who did not receive training (Cohen's d=-0.95, p=0.02), and moderately slower than those conventionally trained (Cohen's d=0.65, p=0.14). However, this difference was not statistically significant. Surgeons trained on extended reality demonstrated a statistically significant improvement in GEARS scores over those who did not train (Cohen's d=0.964, p<0.001). While surgeons trained in extended reality had comparable GEARS scores to surgeons trained conventionally (Cohen's d=0.65, p=0.14). This meta-analysis demonstrates that extended reality simulators translated complex skills to surgeons in a low cost and low risk environment.
△ Less
Submitted 22 January, 2025;
originally announced March 2025.
-
Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl
Authors:
Mark Bickford
Abstract:
This article is the first in a series of articles that explain the formalization of a constructive model of cubical type theory in Nuprl. In this document we discuss only the parts of the formalization that do not depend on the choice of base category. So, it spells out how we make the first steps of our formalization of cubical type theory.
This article is the first in a series of articles that explain the formalization of a constructive model of cubical type theory in Nuprl. In this document we discuss only the parts of the formalization that do not depend on the choice of base category. So, it spells out how we make the first steps of our formalization of cubical type theory.
△ Less
Submitted 15 June, 2018;
originally announced June 2018.
-
Intuitionistic Completeness of First-Order Logic
Authors:
Robert Constable,
Mark Bickford
Abstract:
We establish completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable if and only if its embedding into minimal logic, mFOL, is uniformly valid under the Brouwer Heyting Kolmogorov (BHK) semantics, the intended semantics of iFOL and mFOL. Our proof is intuitionistic and provides an effective procedure Prf that converts uniform minimal evidence into a formal first…
▽ More
We establish completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable if and only if its embedding into minimal logic, mFOL, is uniformly valid under the Brouwer Heyting Kolmogorov (BHK) semantics, the intended semantics of iFOL and mFOL. Our proof is intuitionistic and provides an effective procedure Prf that converts uniform minimal evidence into a formal first-order proof. We have implemented Prf. Uniform validity is defined using the intersection operator as a universal quantifier over the domain of discourse and atomic predicates. Formulas of iFOL that are uniformly valid are also intuitionistically valid, but not conversely. Our strongest result requires the Fan Theorem; it can also be proved classically by showing that Prf terminates using Konig's Theorem.
The fundamental idea behind our completeness theorem is that a single evidence term evd witnesses the uniform validity of a minimal logic formula F. Finding even one uniform realizer guarantees intuitionistic validity because Prf(F, evd) builds a first-order proof of F, establishing its intuitionistic validity and providing a purely logical normalized realizer.
We establish completeness for iFOL as follows. Friedman showed that iFOL can be embedded in minimal logic (mFOL) by his A-transformation, mapping formula F to FA. If F is uniformly valid, then so is FA, and by our completeness theorem, we can find a proof of FA in minimal logic. Then we intuitionistically prove F from FFalse, i.e. by taking False for A and for \bot of mFOL. Our result resolves an open question posed by Beth in 1947.
△ Less
Submitted 17 October, 2011; v1 submitted 7 October, 2011;
originally announced October 2011.
-
Knowledge-Based Synthesis of Distributed Systems Using Event Structures
Authors:
Mark Bickford,
Robert Constable,
Joseph Halpern,
Sabina Petride
Abstract:
To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. This process is particularly effective if the specifications are written in a high-level language that makes it easy for designers to specify their goals. We consider a high-level specification language that results from a…
▽ More
To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. This process is particularly effective if the specifications are written in a high-level language that makes it easy for designers to specify their goals. We consider a high-level specification language that results from adding knowledge to a fragment of Nuprl specifically tailored for specifying distributed protocols, called event theory. We then show how high-level knowledge-based programs can be synthesized from the knowledge-based specifications using a proof development system such as Nuprl. Methods of Halpern and Zuck then apply to convert these knowledge-based protocols to ordinary protocols. These methods can be expressed as heuristic transformation tactics in Nuprl.
△ Less
Submitted 19 May, 2011; v1 submitted 23 June, 2009;
originally announced June 2009.
