yusuke1997/dblp-id-title huggingface dataset:
Mellow Mushroom: Stay Grounded or Schedulefly?
House4hack: Stimulating Technical and Practical Innovation for Social Good
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq
A Formal C Memory Model for Separation Logic
A Learning-Based Fact Selector for Isabelle/HOL
Eliminating Duplication with the Hyper-Linking Strategy
Parallelization of Deduction Strategies: An Analytical Study
Mechanizing Complemented Lattices Within Mizar Type System
Goal-Oriented Proof-Search in Natural Deduction for Intuitionistic Propositional Logic
The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar
Intelligent Backtracking in Deduction Systems by Means of Extended Unification Graphs
Candle: A Verified Implementation of HOL Light (Extended Version)
The Problem of Explaining the Disparate Performance of Hyperresolution and Paramodulation
Formally Verified Algorithms for Upper-Bounding State Space Diameters
Robot Selection Expert 'Rose'
The Theory of Idempotent Semigroups is of Unification Type Zero
Reusing a JML Specification Dedicated to Verification for Testing, and Vice-Versa: Case Studies
Debugging Incoherent Terminologies
Meeting the Challenge of Fifty Years of Logic
Termination of Nested and Mutually Recursive Algorithms
A Verified ODE Solver and the Lorenz Attractor
The Problem of Demodulator Adjunction
Towards Probabilistic Formal Analysis of SATS-Simultaneously Moving Aircraft (SATS-SMA)
Using Hints to Increase the Effectiveness of an Automated Reasoning Program: Case Studies
Program Verification
A Formalization of Metric Spaces in HOL Light
Clifford Algebraic Reduction Method for Automated Theorem Proving in Differential Geometry
Special Issue Mechanizing and Automating Mathematics: In honour of N.G. de Bruijn - Preface
Verified Compilation of Floating-Point Computations
Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF
Computer Proofs in Gödel's Class Theory with Equational Definitions for Composite and Cross
Conjecture Synthesis for Inductive Theories
A Decidability Result for the Model Checking of Infinite-State Systems
Identification of Inductive Properties during Verification of Synchronous Sequential Circuits
Classification of Finite Fields with Applications
The Hot List Strategy
Clause Weighting Local Search for SAT
Preface - Special Issue of Selected Extended Papers of IJCAR 2014
A Generalization of Analytic Deduction via Labelled Deductive Systems. Part I: Basic Substructural Logics
The 2D Dependency Pair Framework for Conditional Rewrite Systems - Part II: Advanced Processors and Implementation Techniques
On the Complexity of Deduction Modulo Leaf Permutative Equations
Structuring Resolution Proofs by Introducing New Lemmata
Automated Analysis of Operators on State Tables: A Technique for Intelligent Search
Inductive Expansion: A Calculus for Verifying and Synthesizing Functional and Logic Programs
Synthesising Programs with Non-trivial Constants
A Two-Valued Logic for Properties of Strict Functional Programs Allowing Partial Functions
First-Order Temporal Verification in Practice
Priorities on Defaults with Prerequisites, and Their Application in Treating Specificity in Terminological Default Logic
A Ramsey Theorem in Boyer-Moore Logic
A Formally Verified Compiler Back-end
Decidability of Equivalence of Symbolic Derivations
The QSMA Algorithm for Quantifiers in SMT
Data Complexity of Query Answering in Expressive Description Logics via Tableaux
Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
On the Recursive Decomposition Ordering with Lexicographical Status and Other Related Orderings
Temporal Logic CTL + PROLOG
Resolving Contradictions: A Plausible Semantics for Inconsistent Systems
Improving the Efficiency of a Hyperlinking-Based Theorem Prover by Incremental Evaluation with Network Structures
Simplifying Proofs in Fitch-Style Natural Deduction Systems
Selected Extended Papers of ITP 2015: Preface
Structured Monads for Generic First-Order Syntax Metatheory
Formalization of Bernstein Polynomials and Applications to Global Optimization
The Concept and Implementation of Skeletal Plans
A Two-Level Logic Approach to Reasoning About Computations
Polite Combination of Algebraic Datatypes
Genetic Programming + Proof Search = Automatic Improvement
Wort Unification and Transformation of Generalized Equations
The Problem of Choosing the Inference Rule to Employ
Computer-Aided Constructions of Commafree Codes
Representing and Building Models for Decidable Subclasses of Equational Clausal Logic
Methods of Lemma Extraction in Natural Deduction Proofs
New Worst-Case Upper Bounds for SAT
Upside-Down Meta-Interpretation of the Model Elimination Theorem-Proving Procedure for Deduction and Abduction
Explaining AI Decisions Using Efficient Methods for Learning Sparse Boolean Formulae
Formalization of Geometric Algebra in HOL Light
Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity
Reasoning about Solids Using Constraint Logic Programming
Engel's Theorem in Mathlib
Non-Horn Problems
Automated Reasoning in Geometry Theorem Proving with Prolog
Obvious Inferences
Operating System Verification
Interweaving Knowledge Extracting, Organizing and Evaluating: A Concrete Design for Preventing Logic and Structure Bugs while Interviewing Experts
The Problem of Demodulation During Inference Rule Application
Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics
Proof Pearl: The KeY to Correct and Stable Sorting
Formally Proving Size Optimality of Sorting Networks
An Automated Reasoning Problem Associated with Proving Claims about Programs Using Floyd-Hoare Inductive Assertin Methods
Z-Match: An Inference Rule for Incrementally Elaborating Set Instantiations
Introduction to Milestones in Interactive Theorem Proving
A Procedure to Prove Statements in Differential Geometry
Uniform Strategies: The CADE-11 Theorem Proving Contest
Predicate Transformer Semantics for Hybrid Systems
On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic
The GOEDEL Program
Automated Theorem Proving in GeoGebra: Current Achievements
Competing for the AC-Unification Race
Computer-Aided Construction of Finite Geometric Spaces: Automated Verification of Geometric Constraints
Closed-Form Upper Bounds in Static Cost Analysis
sf K n : Architecture, Refinements, Strategies and Experiments
Model-Theoretic Methods in Combined Constraint Satisfiability
Extended Decision Procedure for a Fragment of HL with Binders
A Mechanically Verified Code Generator
Long-Distance Q-Resolution with Dependency Schemes
Autarkic Computations in Formal Proofs
WALDMEISTER - High-Performance Equational Deduction
The Problem of Extending the Set of Support Strategy
On the Completeness of Incidence Calculus
A Complete Uniform Substitution Calculus for Differential Dynamic Logic
System-Level Non-interference of Constant-Time Cryptography. Part I: Model
Safe Autonomy Under Perception Uncertainty Using Chance-Constrained Temporal Logic
A Case Study in Automated Theorem Proving: Finding Sages in Combinatory Logic
Coloring Terms to Control Equational Reasoning
Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations
Faster and More Complete Extended Static Checking for the Java Modeling Language
Semi-Thue Systems with an Inhibitor
A Type-Theoretic Interpretation of Constructive Domain Theory
Proof Generalization in $$\mathrm {LK}$$ LK by Second Order Unifier Minimization
Unification under Associativity and Idempotence is of Type Nullary
The Problem of Choosing between Logic Programming and General-Purpose Automated Reasoning
Quantifier Reordering for QBF
Conquering the Meredith Single Axiom
Dualities Between Alternative Semantics for Logic Programming and Nonmonotonic Reasoning
The Mizar Mathematical Library in OMDoc: Translation and Applications
A Fuzzy Expert System Shell Using Both Exact and Inexact Reasoning
A Machine-Checked Implementation of Buchberger's Algorithm
Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E -Unification
HOL-Boogie - An Interactive Prover-Backend for the Verifying C Compiler
Gazing: An Approach to the Problem of Definition and Lemma Use
Symbolic Execution Proofs for Higher Order Store Programs
Decision Procedures for Elementary Sublanguages of Set Theory: X. Multilevel Syllogistic Extended by the Singleton and Powerset Operators
Reasoning with Nominal Schemas through Absorption
Automated Planning as an Early Verification Tool for Distributed Control
A Parallelization Scheme Based on Work Stealing for a Class of SAT Solvers
Uncertainty Management with Imprecise Knowledge with Application to Design
Quasi-decidability of a Fragment of the First-Order Theory of Real Numbers
Solving Open Problems in Right Alternative Rings with Z-Module Reasoning
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL
Proving Termination of Normalization Functions for Conditional Experessions
State and Progress in Strand Spaces: Proving Fair Exchange
Faster Linear Unification Algorithm
Mechanizing a Process Algebra for Network Protocols
A Solver for Arrays with Concatenation
ABox Abduction in the Description Logic ALC
The Univalence Axiom in Cubical Sets
Guarded Cubical Type Theory
Using Resolution for Testing Modal Satisfiability and Building Models
Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables
From Types to Sets by Local Type Definition in Higher-Order Logic
Tableaux-based Theorem Provers: Systems and Implementations
An Experiment with Satisfiability Modulo SAT
Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting
Correction: Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL
Case Studies of Z-Module Reasoning: Proving Benchmark Theorems from Ring Theory
Saturation-Based Boolean Conjunctive Query Answering and Rewriting for the Guarded Quantification Fragments
Flatterms, Discrimination Nets, and Fast Term Rewriting
A Prover Dealing with Nominals, Binders, Transitivity and Relation Hierarchies
The CADE-13 ATP System Competition
Unification in Datastructure Multisets
Erratum to : Learning-Assisted Automated Reasoning with Flyspeck
Theorem Proving as Constraint Solving for Coherent Logic with Function Symbols
Checking Consistency and Completeness of On-Line Product Manuals
Organizing Numerical Theories Using Axiomatic Type Classes
The Propositional Formula Checker HeerHugo
Regular Language Representations in the Constructive Type Theory of Coq
Ordered Semantic Hyper-Linking
SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment
Selected Extended Papers of VSTTE 2016
An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps
Dealing with Satisfiability and n-ary CSPs in a Logical Framework
Duality for Goal-Driven Query Processing in Disjunctive Deductive Databases
On Preprocessing Techniques and Their Impact on Propositional Model Counting
Combining Induction and Saturation-Based Theorem Proving
Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings
A Decidable First-Order Logic for Knowldge Representation
Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains
Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs
The Linked Inference Principle, I: The Formal Treatment
A PSpace Algorithm for Acyclic Epistemic DL ALCS5 m
The Foundation of a Generic Theorem Prover
Homogeneous Length Functions on Groups: Intertwined Computer and Human Proofs
Single Step Tableaux for Modal Logics
Timed Automata Verification and Synthesis Via Finite Automata Learning
T-Resolution: Refinements and Model Elimination
Local Search Algorithms for SAT: An Empirical Evaluation
An Approach to Systems Verification
What Is Program Synthesis?
A Calculus of Lambda Calculus Contexts
ExpTime Tableaux with Global Caching for Hybrid PDL
Reverse Complexity
Synthesis of Obfuscation Policies to Ensure Privacy and Utility
OWL Reasoning: Subsumption Test Hardness and Modularity
Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness
Java Bytecode Verification: Algorithms and Formalizations
Reducing Protocol Analysis with XOR to the XOR-Free Case in the Horn Theory Based Approach
Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology
On Connections and Higher-Order Logic
Ordered Semantic Hyper Tableaux
The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations - Part 2 - A Survey
Lower Bounds for Runtime Complexity of Term Rewriting
Strategies in Model-Based Diagnosis
Formal Memory Models for the Verification of Low-Level Operating-System Code
A Model-Theoretic Approach for Recovering Consistent Data from Inconsistent Knowledge Bases
A Connection-based Characterization of Bi-intuitionistic Validity
Nicolog: A Simple Yet Powerful cc(FD) Language
Using Typed Lambda Calculus to Implement Formal Systems on a Machine
What Is Automated Reasoning?
Automating Free Logic in HOL, with an Experimental Application in Category Theory
An Assertional Proof of Red-Black Trees Using Dafny
Graph-based Decision for Gödel-Dummett Logics
A Relaxation of Üresin and Dubois' Asynchronous Fixed-Point Theory in Agda
Ordered Model Trees: A Normal Form for Disjunctive Deductive Databases
Nonclassical Logic Theorem Proving
The Problem of Finding a Restriction Strategy More Effective Than the Set of Support Strategy
The problem of hyperparamodulation
Implementing the Davis-Putnam Method
Weak Generalized Closed World Assumption
Improving Legibility of Formal Proofs Based on the Close Reference Principle is NP-Hard
Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm's and Tarski's Theorems
Cyclic Hypersequent System for Transitive Closure Logic
Simplification Orderings: Putting Them to the Test
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
Machine Learning for First-Order Theorem Proving - Learning to Select a Good Heuristic
The HOL Light Theory of Euclidean Space
Nonsystematic Search and No-Good Learning
A Polynomial Model for Logics with a Prime Power Number of Truth Values
A Goal-Directed Decision Procedure for Hybrid PDL
Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic
A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem
Octopus: Combining Learning and Parallel Search
Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book
A Coq Formalization of Lebesgue Integration of Nonnegative Functions
A Sound Framework for delta-Rule Variants in Free-Variable Semantic Tableaux
A New Probabilistic Induction Method
Social Choice Theory in HOL
Encoding Cryptographic Primitives in a Calculus with Polyadic Synchronisation
Partial Functions in ACL2
Superposition for Higher-Order Logic
On Computing Logic Programs
Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover
A Decision Procedure for a Sublanguage of Set Theory Involving Monotone, Additive, and Multiplicative Functions, I: The Two-Level Case
A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm
Preface: Special Issue of Selected Extended Papers of CADE 2019
Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL
Gröbner Bases in Exterior Algebra
Experiments with Semantic Paramodulation
Satchmo - The Compiling and Functional Variants
Missing Proofs Found
Opening the AC-Unification Race
Introduction to the OBDD Algorithm for the ATP Community
A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column
A Proof Theory for Model Checking
Efficient Extensional Binary Tries
Formula Databases for High-Performance Resolution/Paramodulation Systems
Negation as Failure. Completeness of the Query Evaluation Process for Horn Clause Programs with Recursive Definitions
Verified iptables Firewall Analysis and Verification
GRAMY: A Geometry Theorem Prover Capable of Construction
Strongly Typed Term Representations in Coq
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences
A Shortest 2-Basis for Boolean Algebra in Terms of the Sheffer Stroke
Collaborative Planning with Confidentiality
Combination of Uniform Interpolants via Beth Definability
Probably Partially True: Satisfiability for Łukasiewicz Infinitely-Valued Probabilistic Logic and Related Topics
Automated Reasoning in Differential Geometry and Mechanics Using the Characteristic Set Method. Part I. An Improved Version of Ritt-Wu's Decomposition Algorithm
A Proof Procedure for Separation Logic with Inductive Definitions and Data
A Tableau Decision Procedure for SHOIQ
Reasoning about Equality
Automated Proof of Bell-LaPadula Security Properties
Unsolved Problems in Elementary Number Theory
HARP: A Tableau-Based Theorem Prover
Induction Proofs with Partial Functions
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs
Using Well-Founded Relations for Proving Operational Termination
Proving Divide and Conquer Complexities in Isabelle/HOL
Unification in partially commutative semigroups
SAT Modulo Linear Arithmetic for Solving Polynomial Constraints
Logical Cryptanalysis as a SAT Problem
Integrating Computer Algebra into Proof Planning
Automating the Search for Elegant Proofs
TPS: A Theorem-Proving System for Classical Type Theory
A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions
The Problem of Selecting an Approach Based on Prior Success
QPCF: Higher-Order Languages and Quantum Circuits
Some Obstacles to the Automation of Reasoning and the Problem of Redundant Information
Automatic Discovery of Theorems in Elementary Geometry
Markov Chains and Markov Decision Processes in Isabelle/HOL
Preface of Special Issue on "Computer Security: Foundations and Automated Reasoning"
Formalizing Strong Normalization Proofs of Explicit Substitution Calculi in ALF
IJCAR Preface
An Implementation of LF with Coercive Subtyping & Universes
Partial Instantiation Methods for Inference in First-Order Logic
STMM: A Set Theory for Mechanized Mathematics
Replacing Unification by Constraint Satisfaction to Improve Logic Program Expressiveness
Automated Flaw Detection in Algebraic Specifications
Heap-Bounded Assembly Language
Proof-Producing Synthesis of CakeML from Monadic HOL Functions
Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration
Eisbach: A Proof Method Language for Isabelle
An Algorithm to Evaluate Quantified Boolean Formulae and Its Experimental Evaluation
Array Theory of Bounded Elements and its Applications
A Framework for Certified Boolean Branch-and-Bound Optimization
Automated Proofs of the Moufang Identities in Alternative Rings
Reduction and Unification in Lambda Calculi with a General Notion of Subtype
Recursive Program Optimization Through Inductive Synthesis Proof Transformation
Decision Procedures for Elementary Sublanguages of Set Theory: XI. Multilevel Syllogistic Extended by Some Elementary Map Constructs
The Problem of Self-Analytically Choosing the Set of Support
Applying SAT Solving in Classification of Finite Algebras
Unification in Abelian Semigroups
Mechanized Metatheory Revisited
Nagging: A Distributed, Adversarial Search-Pruning Technique Applied to First-Order Inference
In Memory of Mark Stickel
A Unifying View on SMT-Based Software Verification
First-Order Modal Tableaux
The Problem of Finding a Mapping between Clause Representation and Natural-Deduction Representation
Interpolation Systems for Ground Proofs in Automated Deduction: a Survey
The Calculus of Relations as a Foundation for Mathematics
More Church-Rosser Proofs
Computationally Effective Reasoning About Goal Interactions
Autarky Pruning in Propositional Model Elimination Reduces Failure Redundancy
Synthesizing Precise and Useful Commutativity Conditions
A Type System for the Java Bytecode Language and Verifier
A General Setting for Flexibly Combining and Augmenting Decision Procedures
The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover
Automated Reasoning for Security Protocol Analysis
Proof Synthesis and Reflection for Linear Arithmetic
OTTER Experiments in a System of Combinatory Logic
CLIN-S - A Semantically Guided First-Order Theorem Prover
Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints
The Reachability Problem in Constructive Geometric Constraint Solving Based Dynamic Geometry
Decision Procedures for Elementary Sublanguages of Set Theory: XIII. Model Graphs, Reflection and Decidability
An Integral Theorem Prover And The Role Of Proof Planning
ETPS: A System to Help Students Write Formal Proofs
Multi-Completion with Termination Tools
Job-Shop Scheduling Using Automated Reasoning: A Case Study of the Car-Sequencing Problem
A Solution to the PoplMark Challenge Using de Bruijn Indices in Isabelle/HOL
Graph Theory in Coq: Minors, Treewidth, and Isomorphisms
Mechanizing and Improving Dependency Pairs
Local is Best: Efficient Reductions to Modal Logic K
On Rewriting Rules in Mizar
Theorem Proving as Constraint Solving with Coherent Logic
Empirically Successful Automated Reasoning: Systems Issue
Relaxations of the Satisfiability Problem Using Semidefinite Programming
Model Checking Dynamic Memory Allocation in Operating Systems
Extraction of Expansion Trees
Formal Proofs of Hypergeometric Sums - Dedicated to the memory of Andrzej Trybulec
Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant
Unification Types of Completely Regular Semigroups
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL
Combining Nonstably Infinite Theories
A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems
Preface: Logics for Artificial Intelligence
Certified First-Order AC-Unification and Applications
A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering
Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution
Using an Extended PROLOG to Solve the Lion and Unicorn Puzzle
Erratum to: Extension of a Decision Procedure for a Fragment of Hybrid Logic with Binders
Model Completeness, Uniform Interpolants and Superposition Calculus
E-unification with Constants vs. General E-unification
An Efficient Approach to Solving Random k -satProblems
Preface to Special Issue on Reasoning in Description Logics
An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification
"Rippling: Meta-Level Guidance for Mathematical Reasoning, " by Alan Bundy, David Basin, Dieter Hutter, and Andrew Ireland, Cambridge University Press, 2005
Translating Higher-Order Clauses to First-Order Clauses
Boolean Functions as Models for Quantified Boolean Formulas
Formal Verification of C Systems Code
Rewriting with Equivalence Relations in ACL2
Note on McCune's Article on Discrimination Trees
Metalogical Frameworks II: Developing a Reflected Decision Procedure
Optimal Deterministic Controller Synthesis from Steady-State Distributions
The Rue Theorem-Proving System: The Complete Set if LIM+ Challenge Problems
The Area Method - A Recapitulation
Tree Tuple Languages from the Logic Programming Point of View
A Compendium of Continuous Lattices in MIZAR
Triple Dots in a Formal Language
Specification and Verification of Concurrent Programs Through Refinements
A Tableau Based Decision Procedure for an Expressive Fragment of Hybrid Logic with Binders, Converse and Global Modalities
First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice
Integrating Searching and Authoring in Mizar
Efficient Algorithms to Detect and Restore Minimality, an Extension of the Regular Restriction of Resolution
Obituary of Harald Ganzinger
SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs
Optimizing the Clausal Normal Form Transformation
Basic Principles of Mechanical Theorem Proving in Elementary Geometries
Reasoning in Description Logics by a Reduction to Disjunctive Datalog
The Bayesian Ontology Language $$\mathcal {BEL}$$ BEL
Formalization of Shannon's Theorems
Selected Extended Papers of NFM 2017: Preface