The following pages link to (Q3618853):
Displaying 50 items.
- A note on the size of prenex normal forms (Q269710) (← links)
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
- Mark Stickel: his earliest work (Q287332) (← links)
- Guiding Craig interpolation with domain-specific abstractions (Q300418) (← links)
- On the formal analysis of Gaussian optical systems in HOL (Q315313) (← links)
- Formal analysis of optical systems (Q475384) (← links)
- An intuitionistic version of Ramsey's theorem and its use in program termination (Q499082) (← links)
- Linear quantifier elimination (Q707743) (← links)
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
- Proof search algorithm in pure logical framework (Q779163) (← links)
- Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation (Q782499) (← links)
- MetiTarski: An automatic theorem prover for real-valued special functions (Q972422) (← links)
- Formal analysis of continuous-time systems using Fourier transform (Q1640640) (← links)
- Automating regression verification of pointer programs by predicate abstraction (Q1650864) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- Keeping logic in the trivium of computer science: a teaching perspective (Q1696593) (← links)
- On the compressibility of finite languages and formal proofs (Q1706152) (← links)
- On the complexity of the quantified bit-vector arithmetic with binary encoding (Q1708270) (← links)
- Finding read-once resolution refutations in systems of 2CNF clauses (Q1749535) (← links)
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant (Q2051568) (← links)
- Neural precedence recommender (Q2055885) (← links)
- DQBDD: an efficient BDD-based DQBF solver (Q2118347) (← links)
- Verifying the conversion into CNF in dafny (Q2148786) (← links)
- Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light} (Q2198134) (← links)
- Contradiction separation based dynamic multi-clause synergized automated deduction (Q2198231) (← links)
- FTClogic: fuzzy temporal constraint logic (Q2328912) (← links)
- Formal verification of stability and chaos in periodic optical systems (Q2361358) (← links)
- An approximation framework for solvers and decision procedures (Q2362497) (← links)
- Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation (Q2407885) (← links)
- Automated mutual induction proof in separation logic (Q2414251) (← links)
- A modeling and verification framework for optical quantum circuits (Q2418045) (← links)
- Preface to the special issue ``SI: satisfiability modulo theories'' (Q2441769) (← links)
- Efficiently solving quantified bit-vector formulas (Q2441770) (← links)
- Drawing interactive Euler diagrams from region connection calculus specifications (Q2629218) (← links)
- Handbook of automated reasoning. In 2 vols (Q2724150) (← links)
- Geometrisation of first-order logic (Q2795295) (← links)
- Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams (Q2818019) (← links)
- Checking Proofs (Q2950035) (← links)
- (Q3151326) (← links)
- NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability (Q3386749) (← links)
- Towards Formal Fault Tree Analysis Using Theorem Proving (Q3453105) (← links)
- Beagle – A Hierarchic Superposition Theorem Prover (Q3454107) (← links)
- NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF (Q5001547) (← links)
- Programming and verifying a declarative first-order prover in Isabelle/HOL (Q5145439) (← links)
- The Complexity of Finding Read-Once NAE-Resolution Refutations (Q5224491) (← links)
- On the Formalization of Cardinal Points of Optical Systems (Q5348536) (← links)
- (Q5376657) (← links)
- (Q5875427) (← links)
- Evaluation of anonymity and confidentiality protocols using theorem proving (Q5962971) (← links)
- An Impossible Asylum (Q6042557) (← links)
