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.

Rewriting Environment for Arithmetic Circuit Verification: Label: en
Parse Condition: Symbolic Encoding of LL(1) Parsing: Label: en
Knowledge Compilation meets Uniform Sampling: Label: en
The Triguarded Fragment of First-Order Logic: Label: en
A Theory of Satisfiability-Preserving Proofs in SAT Solving: Label: en
A Verified Theorem Prover Backend Supported by a Monotonic Library: Label: en
Automatic Space Bound Analysis for Functional Programs with Garbage Collection: Label: en
SMTS: Distributed, Visualized Constraint Solving: Label: en
Polymorphic success types for Erlang: Label: en
Alternating Reachability Games with Behavioral and Revenue Objectives: Label: en
Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse: Label: en
Towards Smarter MACE-style Model Finders: Label: en
A Complete Cyclic Proof System for Inductive Entailments in First Order Logic: Label: en
Lookahead-Based SMT Solving: Label: en
Loop Analysis by Quantification over Iterations: Label: en
Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing: Label: en
LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems: Label: en
The Weak Completion Semantics and Equality: Label: en
Graph Path Orderings: Label: en
Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm: Label: en
Left-Handed Completeness for Kleene algebra, via Cyclic Proofs: Label: en
The involutions-as-principal types/application-as-unification Analogy: Label: en
Quasipolynomial Set-Based Symbolic Algorithms for Parity Games: Label: en
Two-variable First-Order Logic with Counting in Forests: Label: en
Reasoning About Prescription and Description Using Prioritized Default Rules: Label: en
Efficient SAT-Based Encodings of Conditional Cardinality Constraints: Label: en
A Verified Efficient Implementation of the LLL Basis Reduction Algorithm: Label: en
Why These Automata Types?: Label: en
Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets: Label: en
Decidable Inequalities over Infinite Trees: Label: en
Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic: Label: en
Matching in the Description Logic FL0 with respect to General TBoxes: Label: en
Function Summarization Modulo Theories: Label: en
When Are Two Gossips the Same?: Label: en
Playing with the Maximum-Flow Problem: Label: en
Verification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions: Label: en
Formally Proving the Boolean Pythagorean Triples Conjecture: Label: en
Reasoning about Translation Lookaside Buffers: Label: en
Coq without Type Casts: A Complete Proof of Coq Modulo Theory: Label: en
A One-Pass Tree-Shaped Tableau for LTL+Past: Label: en
A uniform framework for substructural logics with modalities: Label: en
Bunched Hypersequent Calculi for Distributive Substructural Logics: Label: en
Gödel logics and the fully boxed fragment of LTL: Label: en
Proving uniformity and independence by self-composition and coupling: Label: en
Quantified Heap Invariants for Object-Oriented Programs: Label: en
Synchronizing Constrained Horn Clauses: Label: en
A Quantitative Partial Model-Checking Function and Its Optimisation: Label: en
Parallel Graph Rewriting with Overlapping Rules: Label: en
From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes: Label: en
Higher order interpretation for higher order complexity: Label: en