The following pages link to Journal of Automated Reasoning (Q174771):
Displayed 50 items.
- Preface: Special issue on interpolation (Q286728) (← links)
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs (Q286731) (← links)
- Proof tree preserving tree interpolation (Q286737) (← links)
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
- Automated theorem proving in GeoGebra: current achievements (Q286780) (← links)
- The 2013 evaluation of SMT-COMP and SMT-LIB (Q286784) (← links)
- MaLeS: a framework for automatic tuning of automated theorem provers (Q286787) (← links)
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- Erratum to: ``Extension of a decision procedure for a fragment of hybrid logic with binders'' (Q286791) (← links)
- Andrzej Trybulec -- in memoriam (1941--2013) (Q286793) (← links)
- Four decades of {\textsc{Mizar}}. Foreword (Q286794) (← links)
- Reconsidering pairs and functions as sets (Q286796) (← links)
- Mechanizing complemented lattices within Mizar type system (Q286797) (← links)
- Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec (Q286798) (← links)
- MizAR 40 for Mizar 40 (Q286800) (← links)
- Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization (Q286801) (← links)
- Evidence algorithm and inference search in first-order logics (Q286802) (← links)
- Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver (Q286803) (← links)
- Improving legibility of formal proofs based on the close reference principle is NP-hard (Q286805) (← links)
- Symbolic execution proofs for higher order store programs (Q287265) (← links)
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems (Q287269) (← links)
- Decision procedures for flat array properties (Q287272) (← links)
- Interpolation systems for ground proofs in automated deduction: a survey (Q287275) (← links)
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (Q287277) (← links)
- Reverse complexity (Q287279) (← links)
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- Automated proofs of block cipher modes of operation (Q287326) (← links)
- In memory of Mark Stickel (Q287330) (← links)
- Mark Stickel: his earliest work (Q287332) (← links)
- Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
- An experiment with satisfiability modulo SAT (Q287334) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Interactive theorem proving. Preface of the special issue (Q287356) (← links)
- On definitions of constants and types in HOL (Q287358) (← links)
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (Q287361) (← links)
- Eisbach: a proof method language for Isabelle (Q287365) (← links)
- Verified abstract interpretation techniques for disassembling low-level self-modifying code (Q287369) (← links)
- Mechanizing a process algebra for network protocols (Q287372) (← links)
- Completeness and decidability results for CTL in constructive type theory (Q287375) (← links)
- A heuristic prover for real inequalities (Q287379) (← links)
- Adding decision procedures to SMT solvers using axioms with triggers (Q287384) (← links)
- Quantifier reordering for QBF (Q287386) (← links)
- Proving tight bounds on univariate expressions with elementary functions in Coq (Q331615) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization (Q331619) (← links)
- ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching (Q352943) (← links)
- A two-valued logic for properties of strict functional programs allowing partial functions (Q352946) (← links)
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- Multi-completion with termination tools (Q352956) (← links)
- Uncurrying for termination and complexity (Q352959) (← links)