Pages that link to "Item:Q1331625"
From MaRDI portal
The following pages link to Isabelle. A generic theorem prover (Q1331625):
Displaying 42 items.
- The undecidability of proof search when equality is a logical connective (Q2134939) (← links)
- Symbolic automatic relations and their applications to SMT and CHC solving (Q2145347) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Limited second-order functionality in a first-order setting (Q2303245) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Formalization of geometric algebra in HOL Light (Q2323452) (← links)
- Morphism axioms (Q2402279) (← links)
- A survey on temporal logics for specifying and verifying real-time systems (Q2418645) (← links)
- Verifying a scheduling protocol of safety-critical systems (Q2424721) (← links)
- Decidability of bounded higher-order unification (Q2456577) (← links)
- An approach to automatic deductive synthesis of functional programs (Q2457802) (← links)
- On the mechanization of the proof of Hessenberg's theorem in coherent logic (Q2471743) (← links)
- Rewriting conversions implemented with continuations (Q2655323) (← links)
- Admissibility of structural rules for contraction-free systems of intuitionistic logic (Q2710593) (← links)
- Compensation methods to support cooperative applications: A case study in automated verification of schema requirements for an advanced transaction model (Q2744791) (← links)
- Automating Soundness Proofs (Q2810691) (← links)
- Towards an Awareness-Based Semantics for Security Protocol Analysis (Q2841215) (← links)
- A Representation of Fω in LF (Q2841235) (← links)
- Ours Is to Reason Why (Q2842639) (← links)
- A Meta Linear Logical Framework (Q2871843) (← links)
- Narrowing and Rewriting Logic: from Foundations to Applications (Q2873786) (← links)
- A Proof Theoretic Interpretation of Model Theoretic Hiding (Q2890327) (← links)
- Towards Logical Frameworks in the Heterogeneous Tool Set Hets (Q2890328) (← links)
- Proofs and Reconstructions (Q2964467) (← links)
- Formalization of Entropy Measures in HOL (Q3088009) (← links)
- Composable Discovery Engines for Interactive Theorem Proving (Q3088022) (← links)
- Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL (Q3102733) (← links)
- Extracting a DPLL Algorithm (Q3178287) (← links)
- Translating a Dependently-Typed Logic to First-Order Logic (Q3184740) (← links)
- Machine-Checked Proof-Theory for Propositional Modal Logics (Q3305555) (← links)
- Formal Logic Definitions for Interchange Languages (Q3453113) (← links)
- Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers (Q3454091) (← links)
- Trustworthy Graph Algorithms (Invited Talk) (Q5092359) (← links)
- A User-friendly Interface for a Lightweight Verification System (Q5170234) (← links)
- Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Proverʼs Palette (Q5170239) (← links)
- Representing Model Theory in a Type-Theoretical Logical Framework (Q5170290) (← links)
- PVS Embedding of cCSP Semantic Models and Their Relationship (Q5178979) (← links)
- A Theoretical Framework for the Higher-Order Cooperation of Numeric Constraint Domains (Q5179011) (← links)
- (Q5875421) (← links)
- (Q5875430) (← links)
- The formal verification of the ctm approach to forcing (Q6151819) (← links)
- Towards automated deduction in cP systems (Q6154793) (← links)
