BibSLEIGH — Nachum

Travelled to:

1 × Australia
1 × Czech Republic
1 × Israel
1 × Poland
1 × Portugal
1 × Sweden
15 × USA
2 × Austria
2 × Canada
2 × Germany
2 × Japan
2 × United Kingdom
3 × Spain
4 × France
4 × Italy

Collaborated with:

∅ L.Bachmair Z.Hanna Z.Manna J.Jouannaud S.Mitra A.Nadel J.W.Klop G.Sivakumar N.A.Josephson S.Kaplan D.A.Plaisted M.Okada J.Hsiang J.Katz L.Wolf M.P.Bonacina I.Tzameret E.C.Ellerman C.Kirchner R.Treinen C.Hoot N.Lindenstrauss Y.Lee J.Kalechstain V.Ryvchin J.Liu T.Hassner A.Blass Y.Gurevich J.E.Dawson R.Goré Y.Zarai T.Lavee

Talks about:

rewrit (15) program (8) termin (7) system (5) abstract (4) problem (4) order (4) infer (4) prove (3) proof (3)

Person: Nachum Dershowitz

DBLP: Dershowitz:Nachum

Facilitated 1 volumes:

Contributed to:

2015

2014

2013

2010

2008

2007

2006

2005

2004

2003

1999

1998

1997

1995

1993

1992

1991

1990

1989

1988

1987

1986

1985

1984

1983

1981

1979

1978

1977

1993

2018

Wrote 51 papers:

SAT-2015-KalechstainRD: Hints Revealed (JK, VR, ND), pp. 71–87.
RTA-TLCA-2014-LiuDJ #analysis #confluence: Confluence by Critical Pair Analysis (JL, ND, JPJ), pp. 287–302.
CSL-2013-Dershowitz: Res Publica: The Universal Model of Computation (ND), pp. 5–10.
ICDAR-2013-HassnerWD: OCR-Free Transcript Alignment (TH, LW, ND), pp. 1310–1314.
ICDAR-2013-ZaraiLDW: Integrating Copies Obtained from Old and New Preservation Efforts (YZ, TL, ND, LW), pp. 47–51.
CSL-2010-BlassDG #algorithm: Exact Exploration and Hanging Algorithms (AB, ND, YG), pp. 140–154.
IJCAR-2008-BonacinaD #canonical: Canonical Inference for Implicational Systems (MPB, ND), pp. 380–395.
IJCAR-2008-Dershowitz #exclamation: Canonicity! (ND), pp. 327–331.
ICALP-2007-DershowitzT #complexity #proving: Complexity of Propositional Proofs Under a Promise (ND, IT), pp. 291–302.
SAT-2007-DershowitzHN #comprehension #satisfiability #towards: Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver (ND, ZH, AN), pp. 287–293.
SAT-2006-DershowitzHN #algorithm #satisfiability #scalability: A Scalable Algorithm for Minimal Unsatisfiable Core Extraction (ND, ZH, AN), pp. 36–41.
DATE-2005-KatzHD #bound #model checking: Space-Efficient Bounded Model Checking (JK, ZH, ND), pp. 686–687.
RTA-2005-Dershowitz: Open. Closed. Open (ND), pp. 376–393.
RTA-2005-DershowitzE #order: Leanest Quasi-orderings (ND, ECE), pp. 32–45.
SAT-2005-DershowitzHK #bound #model checking: Bounded Model Checking with QBF (ND, ZH, JK), pp. 408–414.
SAT-2005-DershowitzHN #heuristic #satisfiability: A Clause-Based Heuristic for SAT Solvers (ND, ZH, AN), pp. 46–60.
ICLP-2004-Dershowitz #abstraction #termination: Termination by Abstraction (ND), pp. 1–18.
LICS-2003-DershowitzK: Abstract Saturation-Based Inference (ND, CK), pp. 65–74.
RTA-1999-DershowitzM: Jeopardy (ND, SM), pp. 16–29.
RTA-1998-DershowitzT #database #online #problem: An On-line Problem Database (ND, RT), pp. 332–342.
RTA-1997-Dershowitz: Innocuous Constructor-Sharing Combinations (ND), pp. 202–216.
ILPS-1995-Dershowitz #semantics: Goal Solving as Operational Semantics (ND), pp. 3–17.
RTA-1995-DershowitzJK #problem: Problems in Rewriting III (ND, JPJ, JWK), pp. 457–471.
RTA-1993-DershowitzH #termination #topic: Topics in Termination (ND, CH), pp. 198–212.
RTA-1993-DershowitzJK #problem: More Problems in Rewriting (ND, JPJ, JWK), pp. 468–487.
CADE-1992-DershowitzMS #convergence #decidability: Decidable Matching for Convergent Systems (ND, SM, GS), pp. 589–602.
ICALP-1991-Dershowitz #horn clause #set: Cononical Sets of Horn Clauses (ND), pp. 267–278.
RTA-1991-DershowitzJK #problem: Open Problems in Rewriting (ND, JPJ, JWK), pp. 445–456.
ALP-1990-DershowitzL #concurrent: An Abstract Concurrent Machine for Rewriting (ND, NL), pp. 318–331.
ALP-1990-DershowitzMS #equation: Equation Solving in Conditional AC-Theories (ND, SM, GS), pp. 283–297.
ICALP-1989-DershowitzKP #infinity #normalisation: Infinite Normal Forms (ND, SK, DAP), pp. 249–262.
POPL-1989-DershowitzK: Rewrite, Rewrite, Rewrite, Rewrite, Rewrite (ND, SK), pp. 250–259.
CADE-1988-DershowitzOS #canonical #term rewriting: Canonical Conditional Rewrite Systems (ND, MO, GS), pp. 538–549.
LICS-1988-DershowitzO #term rewriting: Proof-Theoretic Techniques for Term Rewriting Theory (ND, MO), pp. 104–111.
LICS-1987-BachmairD #first-order #proving #theorem proving: Inference Rules for Rewrite-Based First-Order Theorem Proving (LB, ND), pp. 331–337.
RTA-1987-BachmairD #congruence: Completion for Rewriting Modulo a Congruence (LB, ND), pp. 192–203.
SLP-1987-DershowitzL87 #debugging #deduction: Deductive Debugging (ND, YJL), pp. 298–306.
CADE-1986-BachmairD #termination: Commutation, Transformation, and Termination (LB, ND), pp. 5–20.
LICS-1986-BachmairDH #equation #order #proving: Orderings for Equational Proofs (LB, ND, JH), pp. 346–357.
SLP-1986-JosephsonD86 #implementation: An Implementation of Narrowing: The RITE Way (NAJ, ND), pp. 187–197.
RTA-1985-Dershowitz #termination: Termination (ND), pp. 180–224.
SLP-1985-DershowitzP85 #logic programming: Logic Programming cum Applicative Programming (ND, DAP), pp. 54–66.
ILPC-1984-DershowitzJ84 #logic programming: Logic Programming by Completion (ND, NAJ), pp. 313–320.
ICALP-1983-HsiangD #proving #theorem proving: Rewrite Methods for Clausal and Non-Clausal Theorem Proving (JH, ND), pp. 331–346.
ICALP-1981-Dershowitz #linear #term rewriting #termination: Termination of Linear Rewriting Systems (ND), pp. 448–458.
ICSE-1981-Dershowitz #abstraction #evolution #source code: The Evolution of Programs: Program Abstraction and Instantiation (ND), pp. 79–89.
ICALP-1979-DershowitzM #multi #order #proving #termination: Proving termination with Multiset Orderings (ND, ZM), pp. 188–202.
ICSE-1978-DershowitzM: Inference Rules for Program Annotation (ND, ZM), pp. 158–167.
POPL-1977-DershowitzM #automation #evolution #source code: The Evolution of Programs: A System for Automatic Program Modification (ND, ZM), pp. 144–154.
TAPSOFT-1993-Dershowitz #termination: Trees, Ordinals and Termination (ND), pp. 243–250.
IJCAR-2018-DawsonDG: Well-Founded Unions (JED, ND, RG), pp. 117–133.