Maria Paola Bonacina

Sarah Winkler

Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11, 2022

2021

Integrated Deduction (Dagstuhl Seminar 21371).

[BibT_eX]

[DOI]

Philipp Rümmer

Renate A. Schmidt

Dagstuhl Reports, 2021

Proof Generation in CDSAT.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, 2021

2020

Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness.

[BibT_eX]

[DOI]

Stéphane Graham-Lengrand

Natarajan Shankar

J. Autom. Reason., 2020

SGGS Decision Procedures.

[BibT_eX]

[DOI]

Sarah Winkler

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Theory Combination: Beyond Equality Sharing.

[BibT_eX]

[DOI]

Pascal Fontaine

Christophe Ringeissen

Cesare Tinelli

Proceedings of the Description Logic, Theory Combination, and All That, 2019

2018

Proofs in conflict-driven theory combination.

[BibT_eX]

[DOI]

Stéphane Graham-Lengrand

Natarajan Shankar

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

Parallel Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Parallel Constraint Reasoning., 2018

2017

Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

On Conflict-Driven Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Automated Formal Methods, 2017

Satisfiability Modulo Theories and Assignments.

[BibT_eX]

[DOI]

Stéphane Graham-Lengrand

Natarajan Shankar

Proceedings of the Automated Deduction - CADE 26, 2017

Automated Reasoning for Explainable Artificial Intelligence.

[BibT_eX]

[DOI]

Proceedings of the ARCADE 2017, 2017

2016

Semantically-Guided Goal-Sensitive Reasoning: Model Representation.

[BibT_eX]

[DOI]

J. Autom. Reason., 2016

2015

Interpolation Systems for Ground Proofs in Automated Deduction: a Survey.

[BibT_eX]

[DOI]

Moa Johansson

J. Autom. Reason., 2015

On Interpolation in Automated Theorem Proving.

[BibT_eX]

[DOI]

Moa Johansson

J. Autom. Reason., 2015

On First-Order Model-Based Reasoning.

[BibT_eX]

[DOI]

Viorica Sofronie-Stokkermans

Ulrich Furbach

Proceedings of the Logic, Rewriting, and Concurrency, 2015

2014

Constraint Manipulation in SGGS.

[BibT_eX]

[DOI]

Proceedings of the 28th International Workshop on Unification, 2014

SGGS Theorem Proving: an Exposition.

[BibT_eX]

[DOI]

Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

2013

On Model-Based Reasoning: Recent Trends and Current Developments.

[BibT_eX]

[DOI]

Proceedings of the 28th Italian Conference on Computational Logic, 2013

Canonical Ground Horn Theories.

[BibT_eX]

[DOI]

Nachum Dershowitz

Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2011

On Deciding Satisfiability by Theorem Proving with Speculative Inferences.

[BibT_eX]

[DOI]

Leonardo Mendonça de Moura

Christopher Lynch

J. Autom. Reason., 2011

On Interpolation in Decision Procedures.

[BibT_eX]

[DOI]

Moa Johansson

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2011

2010

Theory decision by decomposition.

[BibT_eX]

[DOI]

J. Symb. Comput., 2010

On theorem proving for program checking: historical perspective and recent developments.

[BibT_eX]

[DOI]

Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2010

2009

New results on rewrite-based satisfiability procedures.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2009

On Deciding Satisfiability by DPLL(G+<i>T</i>) and Unsound Theorem Proving.

[BibT_eX]

[DOI]

Leonardo Mendonça de Moura

Christopher Lynch

Proceedings of the Automated Deduction, 2009

2008

On Variable-inactivity and Polynomial tau-Satisfiability Procedures.

[BibT_eX]

[DOI]

J. Log. Comput., 2008

Canonical Inference for Implicational Systems.

[BibT_eX]

[DOI]

Nachum Dershowitz

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007

Abstract canonical inference.

[BibT_eX]

[DOI]

Nachum Dershowitz

ACM Trans. Comput. Log., 2007

T-Decision by Decomposition.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

2006

Automated Reasoning.

[BibT_eX]

Alberto Martelli

Intelligenza Artificiale, 2006

Rewrite-Based Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the 6th International Workshop on Strategies in Automated Deduction, 2006

Rewrite-Based Satisfiability Procedures for Recursive Data Structures.

[BibT_eX]

[DOI]

Proceedings of the Combined Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006) and the First International Workshop on Probabilistic Automata and Logics (PaUL 2006), 2006

Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

Towards a unified model of search in theorem-proving: subgoal-reduction strategies.

[BibT_eX]

[DOI]

J. Symb. Comput., 2005

On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 5th International Workshop, 2005

2004

Preface.

[BibT_eX]

[DOI]

Thierry Boy de la Tour

Proceedings of the 5th International Workshop on Strategies in Automated Deduction, 2004

2001

Preface: STRATEGIES 2001.

[BibT_eX]

[DOI]

Bernhard Gramlich

Proceedings of the 4th International Workshop on Strategies in Automated Deduction, 2001

Combination of Distributed Search and Multi-search in Peers-mcd.d.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000

A taxonomy of parallel strategies for deduction.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2000

1999

A model and a first analysis of distributed-search contraction-based strategies.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 1999

A Taxonomy of Theorem-Proving Strategies.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence Today: Recent Trends and Developments, 1999

1998

On Semantic Resolution with Lemmaizing and Contraction and a Formal Treatment of Caching.

[BibT_eX]

[DOI]

New Gener. Comput., 1998

On the Modelling of Search in Theorem Proving - Towards a Theory of Strategy Analysis.

[BibT_eX]

[DOI]

Inf. Comput., 1998

Analysis of Distributed-Search Contraction-Based Strategies.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence, European Workshop, 1998

1997

Experiments with subdivision of search in distributed theorem proving.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Parallel Symbolic Computation, 1997

The Clause-Diffusion Theorem Prover Peers-mcd (System Description).

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1997

1996

PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems.

[BibT_eX]

[DOI]

Hantao Zhang

J. Symb. Comput., 1996

On the Reconstruction of Proofs in Distributed Theorem Proving: a Modified Clause-Diffusion Method.

[BibT_eX]

[DOI]

J. Symb. Comput., 1996

A Category-Theoretic Treatment of Automated Theorem Proving.

[BibT_eX]

[DOI]

J. Inf. Sci. Eng., 1996

On Semantic Resolution with Lemmaizing and Contraction.

[BibT_eX]

[DOI]

Proceedings of the PRICAI'96: Topics in Artificial Intelligence, 1996

1995

Towards a Foundation of Completion Procedures as Semidecision Procedures.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1995

Distributed Deduction by Clause-Diffusion: Distributed Contraction and the Aquarius Prover.

[BibT_eX]

[DOI]

J. Symb. Comput., 1995

The Clause-Diffusion Methodology for Distributed Deduction.

[BibT_eX]

[DOI]

Fundam. Informaticae, 1995

1994

On subsumption in distributed derivations.

[BibT_eX]

[DOI]

J. Autom. Reason., 1994

Parallelization of Deduction Strategies: An Analytical Study.

[BibT_eX]

[DOI]

J. Autom. Reason., 1994

Cumulating Search in a Distributed Computing Environment: A Case Study in Parallel Satisfiability.

[BibT_eX]

Hantao Zhang

Proceedings of the First International Symposium on Parallel Symbolic Computation, 1994

On the Reconstruction of Proofs in Distributed Theorem Proving with Contraction: A Modified Clause-Diffusion Method.

[BibT_eX]

Proceedings of the First International Symposium on Parallel Symbolic Computation, 1994

Distributed Theorem Proving by Peers.

[BibT_eX]

[DOI]

William McCune

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993

On Fairness in Distributed Automated Deduction.

[BibT_eX]

[DOI]

Proceedings of the STACS 93, 1993

Distributed Deduction by Clause-Diffusion: The Aquarius Prover.

[BibT_eX]

[DOI]

Proceedings of the Design and Implementation of Symbolic Computation Systems, 1993

1992

On Rewrite Programs: Semantics and Relationship with Prolog.

[BibT_eX]

[DOI]

J. Log. Program., 1992

1991

On Fairness of Completion-Based Theorem Proving Strategies.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 4th International Conference, 1991

1990

Operational and Denotational Semantics of Rewrite Programs.

[BibT_eX]

Proceedings of the Logic Programming, Proceedings of the 1990 North American Conference, Austin, Texas, USA, October 29, 1990

A System for Distributed Simplification-Based Theorem Proving.

[BibT_eX]

Proceedings of the Parallelization in Inference Systems, 1990

Completion Procedures as Semidecision Procedures.

[BibT_eX]

[DOI]

Proceedings of the Conditional and Typed Rewriting Systems, 1990

An Application of Automated Equational Reasoning to Many-valued Logic.

[BibT_eX]

[DOI]

Siva Anantharaman

Proceedings of the Conditional and Typed Rewriting Systems, 1990

1989

KBlab: An Equational Theorem Prover for the Macintosh.

[BibT_eX]

[DOI]