scientific article
From MaRDI portal
Publication:3618853
zbMath1178.03001MaRDI QIDQ3618853
No author found.
Publication date: 2 April 2009
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (51)
A note on the size of prenex normal forms ⋮ Formal verification of stability and chaos in periodic optical systems ⋮ An approximation framework for solvers and decision procedures ⋮ A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle ⋮ Mark Stickel: his earliest work ⋮ Guiding Craig interpolation with domain-specific abstractions ⋮ Drawing interactive Euler diagrams from region connection calculus specifications ⋮ Towards Formal Fault Tree Analysis Using Theorem Proving ⋮ Beagle – A Hierarchic Superposition Theorem Prover ⋮ On the formal analysis of Gaussian optical systems in HOL ⋮ Formal analysis of continuous-time systems using Fourier transform ⋮ Verifying the conversion into CNF in dafny ⋮ Automating regression verification of pointer programs by predicate abstraction ⋮ Formalization of the resolution calculus for first-order logic ⋮ Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation ⋮ Automated mutual induction proof in separation logic ⋮ Checking Proofs ⋮ A modeling and verification framework for optical quantum circuits ⋮ On the Formalization of Cardinal Points of Optical Systems ⋮ An Impossible Asylum ⋮ A multi-clause dynamic deduction algorithm based on standard contradiction separation rule ⋮ On the formalization of the heat conduction problem in HOL ⋮ Keeping logic in the trivium of computer science: a teaching perspective ⋮ Unnamed Item ⋮ Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light} ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ On the compressibility of finite languages and formal proofs ⋮ On the complexity of the quantified bit-vector arithmetic with binary encoding ⋮ Unnamed Item ⋮ Preface to the special issue ``SI: satisfiability modulo theories ⋮ Efficiently solving quantified bit-vector formulas ⋮ Formal analysis of optical systems ⋮ Programming and verifying a declarative first-order prover in Isabelle/HOL ⋮ An intuitionistic version of Ramsey's theorem and its use in program termination ⋮ Finding read-once resolution refutations in systems of 2CNF clauses ⋮ MetiTarski: An automatic theorem prover for real-valued special functions ⋮ Linear quantifier elimination ⋮ GEOMETRISATION OF FIRST-ORDER LOGIC ⋮ Evaluation of anonymity and confidentiality protocols using theorem proving ⋮ N. G. de Bruijn's contribution to the formalization of mathematics ⋮ Distilling the requirements of Gödel's incompleteness theorems with a proof assistant ⋮ Unnamed Item ⋮ Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams ⋮ NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability ⋮ Neural precedence recommender ⋮ The Complexity of Finding Read-Once NAE-Resolution Refutations ⋮ Proof search algorithm in pure logical framework ⋮ Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation ⋮ FTClogic: fuzzy temporal constraint logic ⋮ NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF ⋮ DQBDD: an efficient BDD-based DQBF solver
Uses Software
This page was built for publication:
