`Travelled to:`

1 × Australia

1 × Finland

1 × France

1 × Germany

1 × Japan

1 × United Kingdom

2 × USA

`Collaborated with:`

M.Koshimura H.Fujita K.Inoue Y.Shirai Y.Ohta ∅ R.Hähnle

`Talks about:`

theorem (6) generat (6) model (5) prover (4) constraint (3) prove (2) magic (2) finit (2) horn (2) use (2)

## Person: Ryuzo Hasegawa

### DBLP: Hasegawa:Ryuzo

### Contributed to:

### Wrote 10 papers:

- SAT-2013-FujitaKH #constraints #named #satisfiability
- SCSat: A Soft Constraint Guided SAT Solver (HF, MK, RH), pp. 415–421.
- CADE-2000-HasegawaFK #branch #generative #performance #using
- Efficient Minimal Model Generation Using Branching Lemmas (RH, HF, MK), pp. 184–199.
- CL-2000-HahnleHS #constraints #finite #generative #proving #theorem proving
- Moder Generation Theorem Proving with Finite Interval Constraints (RH, RH, YS), pp. 285–299.
- CADE-1998-OhtaIH #on the #testing
- On the Relationship Between Non-Horn Magic Sets and Relevancy Testing (YO, KI, RH), pp. 333–348.
- CADE-1997-HasegawaIOK #bottom-up #proving #set #theorem proving #top-down
- Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving (RH, KI, YO, MK), pp. 176–190.
- ICLP-1995-Hasegawa #generative #proving #theorem proving
- Model Generation Theorem Provers and Their Applications (RH), p. 7.
- ICLP-1995-ShiraiH #constraints #problem
- Two Approaches for Finite-Domain Constraint Satisfaction Problems — CP and CMGTP (YS, RH), pp. 249–263.
- CADE-1992-HasegawaKF #generative #lazy evaluation #named #parallel #proving #theorem proving
- MGTP: A Parallel Theorem Prover Based on Lazy Model Generation (RH, MK, HF), pp. 776–780.
- CADE-1992-InoueKH #generative #proving #theorem proving
- Embedding Negation as Failure into a Model Generation Theorem Prover (KI, MK, RH), pp. 400–415.
- ICLP-1991-FujitaH #algorithm #generative #proving #theorem proving #using
- A Model Generation Theorem Prover in KL1 Using a Ramified -Stack Algorithm (HF, RH), pp. 535–548.