CADE-30: 30TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION

This page contains an index consisting of author-provided keywords.

(
(ground) first-order logic	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
A
Action	Action Planning == Wish List
AGMV	The TPTP Format for Interpretations
AI	Singular points of plane curves obtained from geometric constructions: automated methods in man-and-machine collaboration
Algebraic geometry	Is a regular polygon determined by its diagonals? Proving theorems on regular polygons by elimination --- the elementary way
ARGO Group	Automating Geometry Construction Problems
arithmetic	Learning Conjecturing from Scratch
Arrays	What's Decidable About Arrays With Sums?
Artificial intelligence	Towards automatic detection of geometric difficulty of geometry problems
ATP	Interoperability of Proof systems with SC-TPTP (System Description)
automated deduction	Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics Geometry Machine Revisited
Automated deduction in geometry	A Generator of Geometry Deductive Database Method Provers Towards a Structural Analysis of Interesting Geometric Theorems: Analysis of a Survey Towards automatic detection of geometric difficulty of geometry problems
Automated Deduction in Geometry	Automating Geometry Construction Problems
Automated methods	Singular points of plane curves obtained from geometric constructions: automated methods in man-and-machine collaboration
automated reasoning	From Modal Sequent Calculi to Modal Resolution Teaching Automated Deduction: an Implementation-BasedApproach with Maude Computing loci with GeoGebra Discovery: some issues and suggestions
automated reasoning	TBA
Automated Theorem Proving	Faithful Logic Embeddings in HOL – Deep and Shallow Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories Towards the Verification of Higher-Order Logic Automated Reasoning Premise Selection with the Alternating-Path-Method
automation	An Automated Approach towards Constructivizing the GeoCoq Library
axiom systems	ADG-Lib Initiative
Axiomatic Systems	Teaching Axiomatic Systems and Metatheory in Isabelle
Axiomatics	Formalizing Axiomatics for First-Order Logic
B
basic path logic	Applying SCAN to Basic Path Logic and the Ordered Fragment (Extended Abstract)
box folding	Unfolding Boxes with Local Constraints
C
Call-by-value	A Fresh Inductive Approach to Useful Call-by-Value Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs
Cardinality Constraints	Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
Certificate	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Ceva Menelaus Proof	Manifold-based Proving Methods in Projective Geometry
Classical higher-order logic	Faithful Logic Embeddings in HOL – Deep and Shallow
Clausal Connection	The TPTP Format for Clausal Connection Tableau Proofs
Clause Selection	Efficient Neural Clause-Selection Reinforcement
Cluster	StarExec-ARC
Coding scheme	Reinforcing students’ proof structure with Waterproof: an analysis
common unfoldings	Unfolding Boxes with Local Constraints
Competition	The ProoVer Competition at IJCAR 2026
Concrete Domains	Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
Condensed detachment	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Conditional rewriting	Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems
Confluence	Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting
Congruence Closure	Computing Ground Congruence Classes
conjecturing	Learning Conjecturing from Scratch
Constrained Horn Clauses	Infinite State Model Checking by Learning Transitive Relations
Construction Problems	Automating Geometry Construction Problems
constructivization	An Automated Approach towards Constructivizing the GeoCoq Library
Coq/Rocq	On the Coq/Rocq Mechanization of Beeson's "On the Notion of Equal Figures in Euclid"
Cut Elimination Theorem	Cut Elimination for Negative Free Logics with Definite Descriptions
Cylindrical Algebraic Decomposition	More is Less: Adding Polynomials for Faster Explanations in NLSAT Solving Non-Linear Optimization with the Cylindrical Algebraic Covering Method
D
data structure	Verified Path Indexing
decidable fragment of first-order logic	Invariant Synthesis: Decidable Fragments to the Rescue
Decision procedures	What's Decidable About Arrays With Sums?
deductive database method	A Generator of Geometry Deductive Database Method Provers
Dedukti	Vampire and Dedukti
Deduktionstreffen	TBA TBA
Deep and shallow logic embeddings	Faithful Logic Embeddings in HOL – Deep and Shallow
Deep Reinforcement Learning	Efficient Neural Clause-Selection Reinforcement
Definite Descriptions	Cut Elimination for Negative Free Logics with Definite Descriptions
dependency pairs	Lexicographic Combination of Reduction Pairs Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs
Derivations	Review of the TPTP format for derivations
Description Logic	Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT
Description Logics	Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
Differential dynamic logic	A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
Differential-algebraic equations	A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
Dynamic Geometry	Computing loci with GeoGebra Discovery: some issues and suggestions Singular points of plane curves obtained from geometric constructions: automated methods in man-and-machine collaboration
E
Educational research	Reinforcing students’ proof structure with Waterproof: an analysis
Elimination	Is a regular polygon determined by its diagonals? Proving theorems on regular polygons by elimination --- the elementary way
empty triangles	Inference Maximizing Point Configurations for Parsimonious Algorithms
Enumeration	Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration
Envelopes	Singular points of plane curves obtained from geometric constructions: automated methods in man-and-machine collaboration
equal figures	On the Coq/Rocq Mechanization of Beeson's "On the Notion of Equal Figures in Euclid"
equational reasoning	Anti-pattern templates Computing Ground Congruence Classes Planning with Equality
Equational theories	Equational Reasoning Modulo Commutativity in Languages with Binders
Equisatisfiable	Equisatisfiable Inferences
Equivalence closure	Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
Euclid's Elements	On the Coq/Rocq Mechanization of Beeson's "On the Notion of Equal Figures in Euclid"
evaluation strategies	A Fresh Inductive Approach to Useful Call-by-Value
Experiments	StarExec-ARC
F
Faithfulness	Faithful Logic Embeddings in HOL – Deep and Shallow
First-Order Automated Reasoning	Computing Ground Congruence Classes
first-order logic	Teaching Automated Deduction: an Implementation-BasedApproach with Maude Conflict-based Literal Model Generation Formalizing Axiomatics for First-Order Logic
first-order logic	TBA
first-order reasoning	Premise Selection with the Alternating-Path-Method
first-order theorem proving	Planning with Equality
Formal Models	Evaluating LLMs on Formal Models Coursework
formalization	On the Coq/Rocq Mechanization of Beeson's "On the Notion of Equal Figures in Euclid"
Formalized mathematics	IsaGeoCoq, a port of GeoCoq with Isabelle/HOL
Format	Review of the TPTP format for derivations
Formula equations	Computing Witnesses Using the SCAN Algorithm
G
GDV and GDV-LP	Proof Verification with GDV and GDV-LP
gelernter	Geometry Machine Revisited
Generalized Term Rewriting Systems	Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems
gentle theory combination	Being polite is not enough (and other limits of theory combination)
GeoGebra Discovery	Computing loci with GeoGebra Discovery: some issues and suggestions
Geometric Deductive Database method	Towards automatic detection of geometric difficulty of geometry problems
Geometric Loci	Singular points of plane curves obtained from geometric constructions: automated methods in man-and-machine collaboration
geometric locus	Computing loci with GeoGebra Discovery: some issues and suggestions
Geometry	First-Order Simplification of GeoCoq using Dedukti
geometry machine	Geometry Machine Revisited
Geometry software	Different Types of Locus Dependencies in Solving Geometry Construction Problems
geometry theorem provers	ADG-Lib Initiative
Giac	Computing loci with GeoGebra Discovery: some issues and suggestions
Grammar-based tree compression	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Graph acyclicity	Unfolding Boxes with Local Constraints
Graph connectivity	Unfolding Boxes with Local Constraints
GraphViz	Towards automatic detection of geometric difficulty of geometry problems
ground model extension	Conflict-based Literal Model Generation
H
happy birthday	TBA
hierarchical reasoning	On Symbol Elimination and Uniform Interpolation in Theory Extensions
Higher-order	Higher-order Verification of Skolemization Steps
higher-order automated theorem proving	A Lambda-Superposition Tactic for Isabelle/HOL
Higher-Order Logic	Towards the Verification of Higher-Order Logic Automated Reasoning
Higher-Order Rewriting	Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting
higher-order superposition	A Lambda-Superposition Tactic for Isabelle/HOL
Higher-order term rewriting	Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs
I
IJCAR 2026	The ProoVer Competition at IJCAR 2026
IMO	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Implicitization	Singular points of plane curves obtained from geometric constructions: automated methods in man-and-machine collaboration
Incidence Theorems	Manifold-based Proving Methods in Projective Geometry
induction	Learning Conjecturing from Scratch
inductive invariant	Invariant Synthesis: Decidable Fragments to the Rescue
Inferences	Equisatisfiable Inferences
Innermost termination	Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs
Instantiations	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Interactive and automated theorem proving	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
interactive theorem proving	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm Verified Path Indexing IsaGeoCoq, a port of GeoCoq with Isabelle/HOL
Interactive Website	Evaluating LLMs on Formal Models Coursework
Interesting Geometric Theorems	Towards a Structural Analysis of Interesting Geometric Theorems: Analysis of a Survey
interpolation	On Symbol Elimination and Uniform Interpolation in Theory Extensions
Interpretations	The TPTP Format for Interpretations
Invariant	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
invited talk	TBA TBA TBA
Isabelle Proof Assistant	Teaching Axiomatic Systems and Metatheory in Isabelle
Isabelle/HOL	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL A Lambda-Superposition Tactic for Isabelle/HOL
Isabelle/HOL Proof Assistant	Formalizing Axiomatics for First-Order Logic
ITP	Interoperability of Proof systems with SC-TPTP (System Description)
K
Knuth-Bendix ordering	Term Ordering Diagrams
L
Lambda Calculus	The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting
lambda-superposition	A Lambda-Superposition Tactic for Isabelle/HOL
LambdaPi	Leo-III and LambdaPi
Languages with binders	Equational Reasoning Modulo Commutativity in Languages with Binders
Large Language Model	Evaluating LLMs on Formal Models Coursework
Larry Wos' 31st problem	Towards a Structural Analysis of Interesting Geometric Theorems: Analysis of a Survey
Lemmas	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Leo-III	Leo-III and LambdaPi
lexicographic path ordering	Term Ordering Diagrams
library of problems	ADG-Lib Initiative
Local Search	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search.
Local Theories	Relatively Complete and Efficient Partial Quantifier Elimination
Locus-dependent problems	Different Types of Locus Dependencies in Solving Geometry Construction Problems
logic	TBA
logical calculi	From Building Blocks to Real SAT Solvers
Logically constrained term rewriting	Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs
M
machine learning	Learning Conjecturing from Scratch
Manifolds	Manifold-based Proving Methods in Projective Geometry
Mathematical knowledge representation	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Mathematics education	Teaching Automated Deduction: an Implementation-BasedApproach with Maude Proving theorems on regular polygons by elimination --- the elementary way Towards automatic detection of geometric difficulty of geometry problems
MCSat	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search.
Metamath	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Metatheory	Teaching Axiomatic Systems and Metatheory in Isabelle
Metis	A Lambda-Superposition Tactic for Isabelle/HOL
Modal Logic	From Modal Sequent Calculi to Modal Resolution
Model Checking	Infinite State Model Checking by Learning Transitive Relations A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Model Finding	Faithful Logic Embeddings in HOL – Deep and Shallow
N
Negative Free Logic	Cut Elimination for Negative Free Logics with Definite Descriptions
Nelson-Oppen	Polite theory combination, an overview
Non-classical logics	Faithful Logic Embeddings in HOL – Deep and Shallow
Non-Left-Linear Rewrite Rules	Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting
Non-Monotonic Logics	From Modal Sequent Calculi to Modal Resolution
non-redundant clause learning	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
Nonlinear Integer Arithmetic	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search.
NuPRL	TBA
O
Offsets	Singular points of plane curves obtained from geometric constructions: automated methods in man-and-machine collaboration
Ontology	Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT
Optimization Modulo Theories	Solving Non-Linear Optimization with the Cylindrical Algebraic Covering Method
order types	Inference Maximizing Point Configurations for Parsimonious Algorithms
ordered fragment	Applying SCAN to Basic Path Logic and the Ordered Fragment (Extended Abstract)
ordered resolution	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
P
paramodulation	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
parsimonious algorithms	Inference Maximizing Point Configurations for Parsimonious Algorithms
Partial Assignments	Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration
Partial Quantifier Elimination	Relatively Complete and Efficient Partial Quantifier Elimination
pattern matching	Anti-pattern templates
planning	Planning with Equality
Planning	Action Planning == Wish List
polite theory combination	Being polite is not enough (and other limits of theory combination) Polite theory combination, an overview
Polynomial Time Algorithm	Relatively Complete and Efficient Partial Quantifier Elimination
premise selection	Premise Selection with the Alternating-Path-Method
Program analysis	Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems
Program Verification	Cazamariposas: Automated Instability Debugging in SMT-based Program Verification
Projective Geometry	Manifold-based Proving Methods in Projective Geometry
proof	The TPTP Format for Tableaux Proofs
Proof	Proof Verification with GDV and GDV-LP
Proof assistant	First-Order Simplification of GeoCoq using Dedukti Reinforcing students’ proof structure with Waterproof: an analysis
Proof assistant systems	Faithful Logic Embeddings in HOL – Deep and Shallow
Proof calculus	A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
Proof Checking	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Proof compression	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Proof Instability	Cazamariposas: Automated Instability Debugging in SMT-based Program Verification
Proof structure	Reinforcing students’ proof structure with Waterproof: an analysis
Proof structuring	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Proof Systems	Interoperability of Proof systems with SC-TPTP (System Description)
Proof Theoretic	Relatively Complete and Efficient Partial Quantifier Elimination
proof transformation	An Automated Approach towards Constructivizing the GeoCoq Library
Proof Verification	Towards the Verification of Higher-Order Logic Automated Reasoning
Proof-producing decision procedure	Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
Proofs	Manifold-based Proving Methods in Projective Geometry
ProoVer	The ProoVer Competition at IJCAR 2026
prover generator	A Generator of Geometry Deductive Database Method Provers
Pythagorean theorem	Is a regular polygon determined by its diagonals? Proving theorems on regular polygons by elimination --- the elementary way
Q
Quantifier elimination	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
R
Rabinowitsch's trick	Proving theorems on regular polygons by elimination --- the elementary way
Rabinowitsch’s trick	Is a regular polygon determined by its diagonals?
Real Algebra	More is Less: Adding Polynomials for Faster Explanations in NLSAT Solving Non-Linear Optimization with the Cylindrical Algebraic Covering Method
Real arithmetic	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
reasoning	TBA
Recurrence Analysis	Infinite State Model Checking by Learning Transitive Relations
redundancy	Partial Redundancy in Saturation
Regular polygons	Is a regular polygon determined by its diagonals?
resolution	Teaching Automated Deduction: an Implementation-BasedApproach with Maude
Resolution Calculi	From Modal Sequent Calculi to Modal Resolution
Rewriting	Analyzing Weighted Abstract Reduction Systems via Semirings
Rocq	First-Order Simplification of GeoCoq using Dedukti An Automated Approach towards Constructivizing the GeoCoq Library
S
Safety	Infinite State Model Checking by Learning Transitive Relations A Theorem Prover Based Approach for SAT-Based Model Checking Certification
sat	Inference Maximizing Point Configurations for Parsimonious Algorithms
SAT encodings	Unfolding Boxes with Local Constraints
SAT implementation	From Building Blocks to Real SAT Solvers
SAT solving	From Building Blocks to Real SAT Solvers
Satisfiability	Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration Anti-pattern templates
Satisfiability modulo theories	Being polite is not enough (and other limits of theory combination) Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
satisfiability modulo theory	Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories
Saturation theorem proving	Computing Witnesses Using the SCAN Algorithm
saturation-based theorem proving	Partial Redundancy in Saturation Term Ordering Diagrams Efficient Neural Clause-Selection Reinforcement
SCAN	Applying SCAN to Basic Path Logic and the Ordered Fragment (Extended Abstract)
SCAN algorithm	Computing Witnesses Using the SCAN Algorithm
SCL	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution Conflict-based Literal Model Generation
Second-order quantifier elimination	Computing Witnesses Using the SCAN Algorithm Applying SCAN to Basic Path Logic and the Ordered Fragment (Extended Abstract)
self-learning	Learning Conjecturing from Scratch
Semantic Difference	Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT
Semantics	Analyzing Weighted Abstract Reduction Systems via Semirings
Semirings	Analyzing Weighted Abstract Reduction Systems via Semirings
Sequent Calculuis	From Modal Sequent Calculi to Modal Resolution
Sequent Calculus	Cut Elimination for Negative Free Logics with Definite Descriptions
shiny theory combination	Being polite is not enough (and other limits of theory combination) Polite theory combination, an overview
Siemens	TBA
simplification ordering	Term Ordering Diagrams
Single Cell Construction	More is Less: Adding Polynomials for Faster Explanations in NLSAT
Singular points	Singular points of plane curves obtained from geometric constructions: automated methods in man-and-machine collaboration
Skolemization	Higher-order Verification of Skolemization Steps
Sledgehammer	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL A Lambda-Superposition Tactic for Isabelle/HOL
SMT	Cazamariposas: Automated Instability Debugging in SMT-based Program Verification Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. On Symbol Elimination and Uniform Interpolation in Theory Extensions SMT and Functional Equation Solving over the Reals: Challenges from the IMO
SMT solvers	What's Decidable About Arrays With Sums?
SMT Solving	More is Less: Adding Polynomials for Faster Explanations in NLSAT Solving Non-Linear Optimization with the Cylindrical Algebraic Covering Method
SNOMED CT	Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT
StarExec-ARC	StarExec-ARC
superposition calculus	Partial Redundancy in Saturation
symbol elimination	On Symbol Elimination and Uniform Interpolation in Theory Extensions
synthetic geometry	IsaGeoCoq, a port of GeoCoq with Isabelle/HOL
T
tableau	The TPTP Format for Tableaux Proofs
Tableau Proofs	The TPTP Format for Clausal Connection Tableau Proofs
Tarski	Computing loci with GeoGebra Discovery: some issues and suggestions
Tarski's axioms	An Automated Approach towards Constructivizing the GeoCoq Library
Tea Party	Welcome
term indexing	Verified Path Indexing
term rewriting	Lexicographic Combination of Reduction Pairs
Termination	The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting Lexicographic Combination of Reduction Pairs Analyzing Weighted Abstract Reduction Systems via Semirings
Theorem proving	A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
theorem proving	TBA
theory combination	Being polite is not enough (and other limits of theory combination) Polite theory combination, an overview
TPTP	The TPTP Format for Tableaux Proofs
TPTP	Review of the TPTP format for derivations Welcome
TPTP Format	The TPTP Format for Clausal Connection Tableau Proofs The TPTP Format for Interpretations
Transition Systems	Infinite State Model Checking by Learning Transitive Relations
Triangle construction	Different Types of Locus Dependencies in Solving Geometry Construction Problems
U
unfailing completion	Planning with Equality
unification	Equational Reasoning Modulo Commutativity in Languages with Binders Anti-pattern templates Verified Path Indexing
uniform interpolation	Applying SCAN to Basic Path Logic and the Ordered Fragment (Extended Abstract)
useful evaluation	A Fresh Inductive Approach to Useful Call-by-Value
V
Vampire	Efficient Neural Clause-Selection Reinforcement
Vampire	Vampire and Dedukti
Verification	Analyzing Weighted Abstract Reduction Systems via Semirings Leo-III and LambdaPi Vampire and Dedukti Equisatisfiable Inferences Invariant Synthesis: Decidable Fragments to the Rescue
Verification	Higher-order Verification of Skolemization Steps Proof Verification with GDV and GDV-LP
verified algorithm	Verified Path Indexing
verified proofs	Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories
W
Welcome	Welcome
Wish List	Action Planning == Wish List
Z
z3	Learning Conjecturing from Scratch

Disclaimer | Powered by EasyChair Smart Program