Entity usage

This page lists pages that use the given entity (e.g. Q42). The list is sorted by descending page ID, so that newer pages are listed first.

Showing below up to 50 results in range #51 to #100.

An approximation framework for solvers and decision procedures: Label: en
Solution validation and extraction for QBF preprocessing: Label: en
The Bayesian ontology language \(\mathcal {BEL}\): Label: en
Automatically proving termination and memory safety for programs with pointer arithmetic: Label: en
Analyzing program termination and complexity automatically with \textsf{AProVE}: Label: en
Preface. Special issue of selected extended papers of IJCAR 2014: Label: en
Finding proofs in Tarskian geometry: Label: en
Analyzing read-once cutting plane proofs in Horn systems: Label: en
A bi-directional extensible interface between Lean and Mathematica: Label: en
A Coq formalization of Lebesgue integration of nonnegative functions: Label: en
Automated reasoning with restricted intensional sets: Label: en
Extensional higher-order paramodulation in Leo-III: Label: en
On the importance of domain model configuration for automated planning engines: Label: en
Automated discovery of geometric theorems based on vector equations: Label: en
Certified quantum computation in Isabelle/HOL: Label: en
Craig interpolation with clausal first-order tableaux: Label: en
Schematic refutations of formula schemata: Label: en
HOL-Boogie -- an interactive prover-backend for the verifying C compiler: Label: en
Crystal: Integrating structured queries into a tactic language: Label: en
Procedural representation of CIC proof terms: Label: en
Declarative representation of proof terms: Label: en
Geometry constructions language: Label: en
Faster and more complete extended static checking for the Java modeling language: Label: en
A formally verified compiler back-end: Label: en
The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0: Label: en
Mechanized semantics for the clight subset of the C language: Label: en
Social choice theory in HOL. Arrow and Gibbard-Satterthwaite: Label: en
Rewriting conversions implemented with continuations: Label: en
Formalizing an analytic proof of the prime number theorem: Label: en
Computer assisted reasoning. A Festschrift for Michael J. C. Gordon: Label: en
General \(E\)-unification with eager variable elimination and a nice cycle rule: Label: en
Boolean functions as models for quantified Boolean formulas: Label: en
Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts: Label: en
A decision procedure for linear ``big O equations: Label: en
Structures for abstract rewriting: Label: en
Theory extension in ACL2(r): Label: en
A decidable first-order logic for knowledge representation: Label: en
A sequent-style model elimination strategy and a positive refinement: Label: en
Modular and incremental automated termination proofs: Label: en
Formal verification of a generic framework to synthesize SAT-provers: Label: en
Obituary: Harald Ganzinger: Label: en
On the mechanization of the proof of Hessenberg's theorem in coherent logic: Label: en
Translating higher-order clauses to first-order clauses: Label: en
Algorithms for computing minimal unsatisfiable subsets of constraints: Label: en
Expression reduction systems with patterns: Label: en
Inferring phylogenetic trees using answer set programming: Label: en
Automated theorem proving in Euler diagram systems: Label: en
Reasoning in description logics by a reduction to disjunctive datalog: Label: en
A tableau decision procedure for \(\mathcal{SHOIQ}\): Label: en
Tractable reasoning and efficient query answering in description logics: The DL-Lite family: Label: en