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 #1 to #50.

Should Decisions in QCDCL Follow Prefix Order?: Label: en
Non-termination in Term Rewriting and Logic Programming: Label: en
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry: Label: en
A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL: Label: en
Combining higher-order logic with set theory formalizations: Label: en
Synthesising programs with non-trivial constants: Label: en
A formal theory of choreographic programming: Label: en
Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version: Label: en
Computer-aided constructions of commafree codes: Label: en
Finding normal binary floating-point factors efficiently: Label: en
Superposition for higher-order logic: Label: en
Correction to: ``Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL: Label: en
Efficient extensional binary tries: Label: en
Optimal deterministic controller synthesis from steady-state distributions: Label: en
Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover: Label: en
Measuring the readability of geometric proofs: the area method case: Label: en
A solver for arrays with concatenation: Label: en
Linear depth deduction with subformula property for intuitionistic epistemic logic: Label: en
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL: Label: en
Formally-verified round-off error analysis of Runge-Kutta methods: Label: en
Formal verification of termination criteria for first-order recursive functions: Label: en
Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments: Label: en
Self-evident automated geometric theorem proving based on complex number identity: Label: en
Bisequent calculus for four-valued quasi-relevant logics: cut elimination and interpolation: Label: en
Binary codes that do not preserve primitivity: Label: en
POSIX lexing with derivatives of regular expressions: Label: en
Rensets and renaming-based recursion for syntax with bindings extended version: Label: en
SCL(EQ): SCL for first-order logic with equality: Label: en
Engel's theorem in Mathlib: Label: en
An automatically verified prototype of the Android permissions system: Label: en
Unifying splitting: Label: en
An automated approach to the Collatz conjecture: Label: en
First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification: Label: en
Finitary type theories with and without contexts: Label: en
Lower bounds for QCDCL via formula gauge: Label: en
Combining stable infiniteness and (strong) politeness: Label: en
Enabling floating-point arithmetic in the Coq proof assistant: Label: en
Reasoning about vectors: satisfiability modulo a theory of sequences: Label: en
Preprocessing of propagation redundant clauses: Label: en
A proof procedure for separation logic with inductive definitions and data: Label: en
Mechanising Gödel-Löb provability logic in HOL light: Label: en
Measure construction by extension in dependent type theory with application to integration: Label: en
Cyclic hypersequent system for transitive closure logic: Label: en
A resolution proof system for dependency stochastic Boolean satisfiability: Label: en
Special issue: Selected papers based on the presentations at the 3rd international joint conference on automated reasoning (IJCAR 2006), Seattle, WA, USA, August 17--20, 2006.: Label: en
OTTER and the Moufang identity problem: Label: en
On the completeness of SLDENF-resolution: Label: en
Model theoretic approach to view updates in deductive databases: Label: en
Some group theoretic examples with completion theorem provers: Label: en
Soundness and completeness proofs by coinductive methods: Label: en