yusuke1997/dblp-id-title huggingface dataset:
On SMT Theory Design: The Case of Sequences
Knowledge Compilation meets Uniform Sampling
Tableaux for Reasoning About Atomic Updates
A Generic Deskolemization Strategy
Decidable Fragments of Many-Sorted Logic
Hybrid Intersection Types for PCF
Bottom-Up Tree Automata with Term Constraints
HORPO with Computability Closure: A Reconstruction
Dual-Priced Modal Transition Systems with Time Durations
A Framework for Splitting BDI Agents
Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
Why Would You Trust B ?
Playing with Quantified Satisfaction
Model Checking Omega-Regular Hyperproperties with AutoHyperQ
Efficient Simulation for Hardware Model Checking
Polymorphic success types for Erlang
Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages
Characterizing Subset Spaces as Bi-topological Structures
How to Fix It: Using Fixpoints in Different Contexts
From Tableaux to Automata for Description Logics
Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
Gödel Logics and Cantor-Bendixon Analysis
Cobra: A Tool for Solving General Deductive Games
The Weak Completion Semantics and Equality
The Consistency of the CADIAG-2 Knowledge Base: A Probabilistic Approach
Infinite, Canonical String Rewriting Systems Generated by Completion
Computing Preferred Answer Sets in Answer Set Programming
An Isabelle-Like Procedural Mode for HOL Light
Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics
Complexity of Terminological Reasoning Revisited
Coping with Selfish On-Going Behaviors
On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control
Model Checking - My 27-Year Quest to Overcome the State Explosion Problem
Inductive Decidability Using Implicit Induction
A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes
Efficient Rule-Matching for Hyper-Tableaux
Automated and Human Proofs in General Mathematics: An Initial Comparison
A Simple Class of Kripke-Style Models in Which Logic and Computation Have Equal Standing
Tree Interpolation in Vampire
Guiding an Instantiation Prover with Graph Neural Networks
Using Causal Relationships to Deal with the Ramification Problem in Action Formalisms Based on Description Logics
On the Equality of Probabilistic Terms
FRIENDLY-WAM: An Interactive Tool to Understand the Compilation of PROLOG
Automated Theorem Provers Help Improve Large Language Model Reasoning
Logical Closures
Binding Logic: Proofs and Models
Towards a Semantics of Unsatisfiability Proofs with Inprocessing
An Efficient Computation of Extended Generalized Closed World Assumption by Support-for-Negation Sets
Decidability of Fair Termination of Gossip Protocols
Gentzen-Type Calculi for Modal Logic S4 with Barcan Formula
Unification in Order-Sorted Type Theory
On QBF Proofs and Preprocessing
On Abstracting the Procedural Behaviour of Logic Programs
Abduction by Non-Experts
Reasoning About Systems with Transition Fairness
On Disallowing Punctual Intervals in Reflexive Semantics of Halpern-Shoham Logic
Sensitivity Analysis of Locked Circuits
Engineering Theories with Z3
Program Extraction in a Logical Framework Setting
CHAT Is Theta(SLG-Wam)
Solving Language Equations and Disequations with Applications to Disunification in Description Logics and Monadic Set Constraints
Algebraic and Model Theoretic Techniques for Fusion Decidability in Modal Logics
Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper)
Parameterized Complexity and Fixed-Parameter Tractability of Description Logic Reasoning
A Machine-Verified Code Generator
Justification-Based Local Search with Adaptive Noise Strategies
Model Checking Games for the Alternation-Free µ-Calculus and Alternating Automata
Boolean Formulas for the Static Identification of Injection Attacks in Java
Automatic Verification of TLA + Proof Obligations with SMT Solvers
Recurrent Reachability Analysis in Regular Model Checking
An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
Termination of Rewriting With Strategy Annotations
Neutralization and Preemtion in Extended Logic Programs
Protocol Verification Via Rigid/Flexible Resolution
Higher-Order Termination: From Kruskal to Computability
Interpolating Quantifier-Free Presburger Arithmetic
Minimal Modifications of Deep Neural Networks using Verification
CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
A Local System for Classical Logic
Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008
A Complete Axiom System for Isomorphism of Types in Closed Categories
Linear Constraints over Infinite Trees
Logic Programming and Automated Reasoning, 5th International Conference, LPAR'94, Kiev, Ukraine, July 16-22, 1994, Proceedings
Simplification of Horn Clauses That Are Clausal Forms of Guarded Formulas
Elementary Lower Bounds for th Length of Refutations
Permutative Additives and Exponentials
Static Analysis of Prolog with Cut
Non-oblivious Strategy Improvement
Automating Verification of Loops by Parallelization
Automating Type Soundness Proofs via Decision Procedures and Guided Reductions
On Bounded Specifications
How Much Should This Symbol Weigh? A GNN-Advised Clause Selection
On the Specification of Sequent Systems
Duality between Merging Operators and Social Contraction Operators
Reasoning About Incompletely Defined Programs
Superposition-Based Analysis of First-Order Probabilistic Timed Automata
A Semantic Basis for Proof Queries and Transformations
Normalisation by Completeness with Heyting Algebras
Reasoning About the Reals: The Marriage of HOL and Maple
A Kind of Achievement by Parts Method
CHIP and Propia
On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
Certifying Synchrony for Free
WAM Specification for Parallel Execution on SIMD Computer
Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings
Games, Probability and the Quantitative µ-Calculus qMµ
A Contextual Logical Framework
Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
The Nullness Analyser of julia
Craig Interpolation for the Integers: Results, Implementation, and Experiences
Automated Reasoning with Tangles: towards Quantum Verification Applications
LPAR 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch, South Africa, Short papers proceedings
Default Logics with Preference Order: Principles and Characterisations
Satisfiability Checking for PC(ID)
A Logic Programming Framework for the Abductive Inference of Intentions in Cooperative Dialogues
RAT Elimination
Derivational Complexity of Knuth-Bendix Orders Revisited
Layered Clausal Resolution in the Multi-modal Logic of Beliefs and Goals
The Separation Theorem for Differential Interaction Nets
Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy
On a Semantic Subsumption Test
A Cooperative Answering System
An excursion to the border of decidability: between two- and three-variable logic
An Adequate Compositional Encoding of Bigraph Structure in Linear Logic with Subexponentials
Logical Foundation for Logic Programming Based on First Order Linear Temporal Logic
Coherent Composition of Distributed Knowledge-Bases Through Abduction
Boolean Functions for Finite-Tree Dependencies
Forgetting for Defeasible Logic
Towards Using the Andorra Kernel Language for Industrial Real-Time Applications
From the Past to the Future: Executing Temporal Logic Programs
Certifying Incremental SAT Solving
A One-Pass Tree-Shaped Tableau for LTL+Past
An Intuitionistic Epistemic Logic for Sequential Consistency on Shared Memory
Static Reduction Analysis for Imperative Object Oriented Languages
Disproving False Conjectures
Fucusing and Proof-Nets in Linear and Non-commutative Logic
Parameter Synthesis for Probabilistic Hyperproperties
Simplifying Binary Propositional Theories into Connected Components Twice as Fast
Automating Coherent Logic
Operational Semantics for Fixed-Point Logics on Constraint Databases
Verification of Switch-Level Designs with Many-Valued Logic
The Triguarded Fragment with Transitivity
Completeness of E-Unification with Eager Variable Elimination
Efficient Structural Information Analysis for Real CLP Languages
Coherence and Transitivity in Coercive Subtyping
A Process Semantics of Logic Programs
A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus
Role Conjunctions in Expressive Description Logics
Proof Plans for the Correction of False Conjectures
Distributed Consistency-Based Diagnosis
Conflict Anticipation in the Search for Graph Automorphisms
On the Complexity of Counting the Hilbert Basis of a Linear Diophnatine System
Tractable Quantified Constraint Satisfaction Problems over Positive Temporal Templates
Symbolic Automata Constraint Solving
Improving On-Demand Strategy Annotations
A Simple Transformation from Prolog-written Metalevel Interpreters into Compilers and its Implementation
Prolog with Arrays and Bounded Quantifications
Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
SAT Solving for Argument Filterings
The Elog Web Extraction Language
The Complexity of Temporal Logic with Until and Since over Ordinals
On Translations of Epsilon Proofs to LK
Abstract Model Generation for Preprocessing Clause Sets
Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002, Proceedings
Representing Defaults and Negative Information Without Negation-as-Failure
A typed parallel lambda-calculus via 1-depth intermediate proofs
Imperative Object-Based Calculi in Co-inductive Type Theories
System Description of LAMBDALG - A Higher Order Algebraic Specification Language
Implementing Connection Calculi for First-order Modal Logics
Value Sensitivity and Observable Abstract Values for Information Flow Control
Gödel logics with an operator shifting truth values
Weak beta-theta-Normalization and Normalization by Evaluation for System F
HoTT-Crypt : A Study in Homotopy Type Theory based on Cryptography
Pushdown Module Checking
Building Proofs by Analogy via the Curry-Horward Isomorphism
Deep Inference in Proof Search: The Need for Shallow Inference
Clausal Proof Compression
Synchronized Recursive Timed Automata
ATP Cross-Verification of the Mizar MPTP Challenge Problems
Resource Management in Linear Logic Search Revisited
SAT Encoding of Unification in EL
Context-Sensitive Multivariant Assertion Checking in Modular Programs
Reasoning about Evolving Nonmonotonic Knowledge Bases
MIZ-PR: A Theorem Prover for Polymorphic and Recursive Functions
Why These Automata Types?
LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023
iSat: Structure Visualization for SAT Problems
Splitting Through New Proposition Symbols
The EKS-V1 System
PBINT, A Logic for Modelling Search Problems Involving Arithmetic
A Generic Framework for Interprocedural Analyses of Numerical Properties
OR-Parallel Theorem Proving with Random Competition
Saturating Sorting without Sorts
Data Complexity in the EL Family of Description Logics
Verifying Temporal Properties in Real Models
On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity
Generalized Negation As Failure and Semantics of Normal Disjunctive Logic Programs
Computable Numberings
The Unification of Infinite Sets of Terms and Its Applications
Deduction with Generalized Terms
Towards Algorithmic Cut-Introduction
Modelling Moral Reasoning and Ethical Responsibility with Logic Programming
Embedding Intuitionistic into Classical Logic
Wayeb: a Tool for Complex Event Forecasting
On Confluence of Infinitary Combinatory Reduction Systems
Programming Cognitive Agents in Defeasible Logic
A Non-commutative Extension of MELL
Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings
A First Order Resolution Calculus with Symmetries
Theory Instantiation
Modular Cut-Elimination: Finding Proofs or Counterexamples
Coq without Type Casts: A Complete Proof of Coq Modulo Theory
Logic Programming and Automated Reasoning,4th International Conference, LPAR'93, St. Petersburg, Russia, July 13-20, 1993, Proceedings
Logic Programming and Automated Reasoning, 6th International Conference, LPAR'99, Tbilisi, Georgia, September 6-10, 1999, Proceedings
Symbolic Realisation of Epistemic Processes
Programming by Composing Filters
On Minimality and Integrity Constraints in Probabilistic Abduction
Default Reasoning in Action Domains with Conditional, Non-Local Effect Actions
Partitioning SAT Instances for Distributed Solving
Integrating Inductive Definitions in SAT
Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
Exploiting Fixable, Removable, and Implied Values in Constraint Satisfaction Problems
The KCM System: Speeding-up Logic Programming through Hardware Support
Query Optimization of Disjunctive Databases with Constraints through Binding Propagation
Infinite Families of Finite String Rewriting Systems and Their Confluence
Implementing a Finite-domain CLP-language on Top of Prolog: a Transformational Approach
LPAR 2024 Complementary Volume, Port Louis, Mauritius, May 26-31, 2024
A Quantitative Partial Model-Checking Function and Its Optimisation
Reasoning in the presence of inconsistency through Preferential ALC
Tableau Calculus for Dummett Logic Based on Present and Next State of Knowledge
A Verified SAT Solver Framework including Optimization and Partial Valuations
PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification
Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings
Gamifying Program Analysis
Reasoning About Loops Using Vampire in KeY
Disunification for Ultimately Periodic Interpretations
Abstract DPLL and Abstract DPLL Modulo Theories
Is Cantor's Theorem Automatic?
First Order Linear Temporal Logic over Finite Time Structures
Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation
Herbrand Theorems for Substructural Logics
A Fast and Accurate ASP Counting Based Network Reliability Estimator
Unification in a Combination of Equational Theories with Shared Constants and its Application to Primal Algebras
Reasoning About Group Polarization: From Semantic Games to Sequent Systems
Representation of Partial Knowledge and Query Answering in Locally Complete Databases
Logical Omniscience and the Cost of Deliberation
Automatic Detection of Vulnerable Variables for CTL Properties of Programs
On Resolution in Fragments of Classical Linear Logic
Formally Proving the Boolean Pythagorean Triples Conjecture
Abstract Syntax and Logic Programming
Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models
Regular Sets of Descendants for Constructor-Based Rewrite Systems
The Use of Planning Critics in Mechanizing Inductive Proofs
A Syntax-Based Approach to Reasoning about Actions and Events
Generic Resolution in Propositional Modal Systems
Reasoning About Embedded Dependencies Using Inclusion Dependencies
Counterfactuals Modulo Temporal Logics
Least and Greatest Fixed Points in Linear Logic
A Nonmonotonic Extension of KLM Preferential Logic P
A Refinement Theory that Supports Reasoning About Knowledge and Time
Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs
Lemma Learning in the Model Evolution Calculus
A Higher-Order Iterative Path Ordering
Handling Equality in Monodic Temporal Resolution
Tableau Calculus for the Logic of Comparative Similarity over Arbitrary Distance Spaces
Lazy Abstraction with Interpolants for Arrays
Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
Nominal Renaming Sets
Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
Search Space Pruning by Checking Dynamic Term Growth
On the Computational Complexity of Spatial Logics with Connectedness Constraints
Solving Graded/Probabilistic Modal Logic via Linear Inequalities (System Description)
On the Complexity of Convex and Reverse Convex Prequadratic Constraints
A Formal Language for Cryptographic Pseudocode
Efficient Generation of Unsatisfiability Proofs and Cores in SAT
Confluence for Proof-Nets via Parallel Cut Elimination
Efficient Evaluation Methods for Guarded Logics and Datalog LITE
Labelled Unit Superposition Calculi for Instantiation-Based Reasoning
Termination of Fair Computations in Term Rewriting
Proof-Search in Implicative Linear Logic as a Matching Problem
Strong Normalization of the Dual Classical Sequent Calculus
Proof-Pattern Recognition and Lemma Discovery in ACL2
Shortening Proofs by Quantifier Introduction
Backward Trace Slicing for Conditional Rewrite Theories
Inference of Termination Conditions for Numerical Loops in Prolog
Combining Lists with Non-stably Infinite Theories
The Complexity of Partial-Observation Parity Games
SKIL: A System for Programming with Proofs
A Comparison of Mechanisms for Avoiding Repetition of Subdeductions in Chain Formal Linear Deduction Systems
Computational Issues in Exploiting Dependent And-Parallelism in Logic Programming: Leftness Detection in Dynamic Search Trees
Cauliflower: a Solver Generator for Context-Free Language Reachability
Proving uniformity and independence by self-composition and coupling
Analytic Tableaux for KLM Preferential and Cumulative Logics
Capability Discovery for Automated Reasoning Systems
Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA
Influence of Variables Encoding and Symmetry Breaking on the Performance of Optimization Modulo Theories Tools Applied to Cloud Resource Selection
Monadic Fragments of Gödel Logics: Decidability and Undecidability Results
Magically Constraining the Inverse Method Using Dynamic Polarity Assignment
Monodic fragments of first-order temporal logics: 2000-2001 A.D
Or-Parallel Prolog with Heuristic Task Distribution
On the Satisfiability of Two-Variable Logic over Data Words
Logic Programming Approaches for Representing and Solving Constraint Satisfaction Problems: A Comparison
IWIL 2012: The 9th International Workshop on the Implementation of Logics, Merida, Venezuela, March 10, 2012
Gandy's Theorem for Abstract Structures without the Equality Test
Proof Planning for Feature Interactions: A Preliminary Report
Querying Proofs
Incremental Integrity Checking: Limitations and Possibilities
Mechanized Verification of CPS Transformations
ProPre A Programming Language with Proofs
Encoding Temporal Logics in Executable Z: A Case Study for the ZETA System
Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
Logic Programming with Pseudo-Resolution
Boosting Local Search Thanks to cdcl
On the Relation between the Lambda-Mu-Calculus and the Syntactic Theory of Sequential Control
Algebraic Intruder Deductions
Interactive Verification of Concurrent Systems using Symbolic Execution
Reducing Nondeterminism in the Calculus of Structures
Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic
Pushdown Specifications
LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020
On Structuring Proof Search for First Order Linear Logic
Second-Order Matching via Explicit Substitutions
Higher-Order Abstract Syntax with Induction in Coq
Short papers for 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning, LPAR-17-short, Yogyakarta, Indonesia, October 10-15, 2010
Linear Objects: a Logic Framework for Open System Programming
A Generic Declarative Diagnoser for Normal Logic Programs
Program Complexity in Hierarchical Module Checking
An Incremental Algorithm to Optimally Maintain Aggregate Views
\mathbb FDNC : Decidable Non-monotonic Disjunctive Logic Programs with Function Symbols
Two-Level Grammar: A Funtional/Logic Query Language for Database and Knowledge-Base Systems
Deciding Key Cycles for Security Protocols
A Partial Evaluation Framework for Curry Programs
Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
Resolution for Many-Valued Logics
Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
The SZS Ontologies for Automated Reasoning Software
How Many Legs Do I Have? Non-Simple Roles in Number Restrictions Revisited
On Implementing Modular Complexity Analysis
Blocked Clause Decomposition
The Relationship Between Reasoning About Privacy and Default Logics
Probabilistic Logic Programs and their Semantics
Finding Periodic Apartments via Boolean Satisfiability and Orderly Generation
Simulating Parity Reasoning
Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
The Equational Theory of < N, 0, 1, +, ×, uparrow > Is Decidable, but Not Finitely Axiomatisable
LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018
Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light
Resolution for Stochastic Boolean Satisfiability
Binding-Time Annotations Without Binding-Time Analysis
On the Use of the Constructive Omega-Rule within Automated Deduction
On Anti-subsumptive Knowledge Enforcement
A Type-Theoretic Approach to Induction with Higher-Order Encodings
Recursive Path Orderings Can Also Be Incremental
Goal Dependent versus Goal Independent Analysis of Logic Programs
A Decomposition Rule for Decision Procedures by Resolution-Based Calculi
Towards Efficient Calculi for Resource-Oriented Deductive Planning
Abstraction-Carrying Code
Proving Infinite Satisfiability
Quantified Propositional Gödel Logics
First Experiments with Neural cvc5
Automatic Generation of Invariants for Circular Derivations in SUP(LA)
A Translation Characterizing the Constructive Content of Classical Theories
An Application to Teaching in Logic Course of ATP Based Natural Deduction
On the Relative Succinctness of Nondeterministic Büchi and co-Büchi Word Automata
Prediction and Explanation over DL-Lite Data Streams
Lambda-Mu-Calculus: An Algorithmic Interpretation of Classical Natural Deduction
Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions
A New Type Theory for Representing Logics
Compiling and Verifying Security Protocols
Functional Pearl: the Proof Search Monad
Playing Logic Programs with the Alpha-Beta Algorithm
Tactic Learning and Proving for the Coq Proof Assistant
Relentful Strategic Reasoning in Alternating-Time Temporal Logic
Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
Parsing with DCG-terms
Playing Lorenzen Dialogue Games on the Web
Whatever Happened to Deductive Question Answering?
Tracking Data-Flow with Open Closure Types
Binding-Time Analysis by Constraint Solving. A Modular and Higher-Order Approach for Mercury
Unification in Order-Sorted Logic With Term Declarations
Reasoning about XML with Temporal Logics and Automata
The TPTP World - Infrastructure for Automated Reasoning
Proofs and Refutations, and Z3
Inference from Controversial Arguments
A WAM Compilation Scheme
Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings
Rotation Based MSS/MCS Enumeration
A Local System for Linear Logic
Polite Theories Revisited
Alternation Elimination by Complementation (Extended Abstract)
Decidable linear list constraints
Function Summarization Modulo Theories
On Computing Constraint Abduction Answers
Enfragmo: A System for Modelling and Solving Search Problems with Logic
Knowledge-Based Synthesis of Distributed Systems Using Event Structures